Theorem (11.48): S ∩ T = {}  ≡  (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
Proof:
  Using “Mutual implication”:
    Subproof for `S ∩ T = {} ⇒ (∀ x • x ∈ S ⇒ ¬ (x ∈ T))`:
      Assuming `S ∩ T = {}`:
          (∀ x • x ∈ S ⇒ ¬ (x ∈ T))
        ≡⟨ ? ⟩
          true
    Subproof for `(∀ x • x ∈ S ⇒ ¬ (x ∈ T)) ⇒ S ∩ T = {}`:
      Assuming `(∀ x • x ∈ S ⇒ ¬ (x ∈ T))`:
          S ∩ T = {}
        ≡⟨ ? ⟩
          true


Theorem (11.69): (∃ x ❙ x ∈ S • ¬ (x ∈ T)) ⇒ S ≠ T
Proof:
  Using “Transitivity of ⇒”:
    Subproof for `(∃ x ❙ x ∈ S • ¬ (x ∈ T)) ⇒ S ≠ T`:
      Assuming `(∃ x ❙ x ∈ S • ¬ (x ∈ T))`:
          S ≠ T
        ≡⟨ “Definition of ≠” ⟩
          ¬ (S = T)
        ≡⟨ ? ⟩
          true
    Subproof for `S ≠ T ⇒ (∃ x ❙ x ∈ S • ¬ (x ∈ T))`:
      Assuming `S ≠ T`:
          (∃ x ❙ x ∈ S • ¬ (x ∈ T))
        ≡⟨ ? ⟩
          true