>>12354194From your attitude this is likely going to seem pointless to you, but lurking anons may appreciate a fleshed-out proof by equational reasoning, applied to the theory of a Boolean algebra. This alternate method is equally valid, and has the advantage of remaining so even when the sets involved cannot be constructed extensionally for whatever reason (e.g. mutable states, infinite memory requirements).
The axioms include, among others, the universal quantifications of the following:
(1 Commutativity) B ? A = A ? B
(2 Associativity) A ? (B ? C) = (A ? B) ? C
(3 Monotonicity of the lattice-theoretic partial order B ? C <=> B = B ? C) B ? C implies A ? B ? A ? C
This is often taken as axiomatic in Heyting algebras, though it follows from the algebraic definition of ? as a meet.
(4 Involutive lattice-theoretic complement) Each A has a unique complement 1\A with 1\(1\A)=A
(5 Antitonicity of complementation) If A ? B then 1\B ? 1\A
In the theory of orthomodular lattices, this is axiomatic. Otherwise, it's a consequence of de Morgan's laws and the lattice-theoretic definitional equivalence A ? B <=> A = A ? B <=> B = A ? B via:
A ? B <=> A = A ? B <=> 1\A = 1\(A ? B) <=> 1\A = 1\A ? 1\B <=> 1\B ? 1\A
Then:
>>B ? C implies B \ A ? C \ A(3) applied to 1\A
>>hence B \ (C \ A) ? B \ (B \ A)(5) applied to B \ A ? C \ A, followed by (3) applied to B
>>B \ (B \ A) = B ? A --(6)(4) applied to the Boolean subalgebra with global maximum B, i.e. the lower set of B. As this does not assume B ? C, it is an identity.
>>B ? A = A ? B(1)
>>C ? A = C \ (C \ A)Application of the identity (6)
>>A ? B = B ? (C ? A)To the antecedent B = B ? C, take meets with A, then apply (1) and (2).
>>B ? (C ? A) = B ? C \ (C \ A)Substitution of the identity (6)
>>B ? C \ (C \ A) ? B \ (C \ A)(3) applied to the lattice identity B ? C ? B
