Theorem (11.48): S ∩ T = {}  ≡  (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
Proof:
    S ∩ T = {}  ≡  (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
  =⟨ “Set extensionality” ⟩
    (∀ x  •  x ∈ (S ∩ T)  ≡  x ∈ {}) ≡ (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
  =⟨ “Empty set” ⟩
    (∀ x  •  x ∈ (S ∩ T)  ≡  false) ≡ (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
  =⟨ “Definition of ¬ from ≡” ⟩
    (∀ x  •  ¬ (x ∈ (S ∩ T))) ≡ (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
  =⟨ “Intersection” ⟩
    (∀ x  •  ¬ (x ∈ S ∧ x ∈ T)) ≡ (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
  =⟨ “De Morgan” ⟩
    (∀ x  • (¬ (x ∈ S) ∨ (¬ (x ∈ T)))) ≡ (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
  =⟨ “Complement” ⟩
    (∀ x  • (¬ (x ∈ S) ∨ (x ∈ ~ T))) ≡ (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
  =⟨ “Definition of ⇒” ⟩
    (∀ x  • ((x ∈ S) ⇒ (x ∈ ~ T))) ≡ (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
  =⟨ “Complement” ⟩
    (∀ x  • ((x ∈ S) ⇒ ¬ (x ∈ T))) ≡ (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
  =⟨ “Reflexivity of ≡” ⟩
    true