Theorem “Subset” “Inclusion”:     S ⊆ T  ≡  (∀ x • x ∈ S ⇒ x ∈ T)
Proof:
    S ⊆ T
  ≡⟨ “Subset” ⟩
   (∀ x ❙ x ∈ S • x ∈ T)
  ≡⟨ “Trading for ∀” ⟩
   (∀ x • x ∈ S ⇒ x ∈ T)







Theorem “Inclusion in empty set”: S ⊆ {}  ≡  S = {}
Proof:
    S ⊆ {}  ≡  S = {}
  ≡⟨ “Subset” and “Set Equality” ⟩
    (∀ e ❙ e ∈ S • e ∈ {}) ≡ (∀ e • e ∈ S ≡ e ∈ {})
  ≡⟨ “Empty set” ⟩
    (∀ e ❙ e ∈ S • false) ≡ (∀ e • e ∈ S ≡ false)
  ≡⟨ “Trading for ∀” ⟩
    (∀ e • e ∈ S ∧ false ≡ e ∈ S) ≡ (∀ e • e ∈ S ≡ false)
  ≡⟨ “Zero of ∧” ⟩
    (∀ e • false ≡ e ∈ S) ≡ (∀ e • e ∈ S ≡ false)
  ≡⟨ “Reflexivity of ≡” ⟩
    true








Theorem “Inclusion of universe”: 𝐔 ⊆ S  ≡  𝐔 = S
Proof:
    𝐔 ⊆ S  ≡  𝐔 = S
  ≡⟨ “Subset” and “Set Equality” ⟩
    (∀ e ❙ e ∈ 𝐔 • e ∈ S) ≡ (∀ e • e ∈ 𝐔 ≡ e ∈ S)
  ≡⟨ “Universal set” ⟩
    (∀ e ❙ true • e ∈ S) ≡ (∀ e • true ≡ e ∈ S)
  ≡⟨ “Trading for ∀” ⟩
    (∀ e • true ∧ e ∈ S ≡ true) ≡ (∀ e • true ≡ e ∈ S)
  ≡⟨ “Identity of ∧” and “Identity of ≡” ⟩
    (∀ e • e ∈ S) ≡ (∀ e • e ∈ S)
  ≡⟨ “Reflexivity of ≡” ⟩
    true








Theorem “Characterisation of set difference”:   A - B ⊆ S  ≡  A ⊆ S ∪ B
Proof:
    A - B ⊆ S
  ≡⟨ “Subset” ⟩
    (∀ e ❙ e ∈ (A - B) • e ∈ S)
  ≡⟨ “Set difference” ⟩
   (∀ e ❙ e ∈ A ∧ ¬ (e ∈ B) • e ∈ S)
  ≡⟨ “Trading” ⟩
   (∀ e ❙ e ∈ A • ¬ ¬ (e ∈ B) ∨ e ∈ S)
  ≡⟨ “Double negation” ⟩
   (∀ e ❙ e ∈ A • (e ∈ B) ∨ e ∈ S)
  ≡⟨ “Union” ⟩
   (∀ e ❙ e ∈ A • e ∈ (B ∪ S))
  ≡⟨ “Subset” ⟩
    A ⊆ S ∪ B








Theorem “Indirect set equality from below”:
    A = B  ≡  (∀ S : set X • S ⊆ A  ≡  S ⊆ B)
Proof:
  Using “Mutual implication”:
    Subproof for `A = B ⇒ (∀ S : set X • S ⊆ A  ≡  S ⊆ B)`:
      Assuming `A = B`:
        For any `S`:
            S ⊆ A  ≡  S ⊆ B
          ≡⟨ Assumption `A = B` ⟩
            S ⊆ B ≡ S ⊆ B
          ≡⟨ “Reflexivity of ≡” ⟩
            true
    Subproof for `(∀ S : set X • S ⊆ A  ≡  S ⊆ B) ⇒ A = B`:
      Assuming `(∀ S : set X • S ⊆ A  ≡  S ⊆ B)`:
          true
        ≡⟨ “Antisymmetry of ⊆” ⟩
          B ⊆ A ⇒ A ⊆ B ⇒ A = B
        ≡⟨ substitution and Assumption `(∀ S : set X • S ⊆ A  ≡  S ⊆ B)` ⟩
          B ⊆ B ⇒ A ⊆ A ⇒ A = B
        ≡⟨ “Reflexivity of ⊆” and “Left-identity of ⇒” ⟩
          A = B







Theorem “Indirect set equality from above”:
    A = B  ≡  (∀ S : set X • A ⊆ S  ≡  B ⊆ S)
Proof:
  Using “Mutual implication”:
    Subproof for `A = B ⇒ (∀ S : set X • A ⊆ S  ≡  B ⊆ S)`:
      Assuming `A = B`:
        For any `S`:
            A ⊆ S  ≡  B ⊆ S
          ≡⟨ Assumption `A = B` ⟩
            B ⊆ S ≡ B ⊆ S
          ≡⟨ “Reflexivity of ≡” ⟩
            true
    Subproof for `(∀ S : set X • A ⊆ S  ≡  B ⊆ S) ⇒ A = B`:
      Assuming `(∀ S : set X • A ⊆ S  ≡  B ⊆ S)`:
           true
        ≡⟨ “Antisymmetry of ⊆” ⟩
          B ⊆ A ⇒ A ⊆ B ⇒ A = B
        ≡⟨ Assumption `(∀ S : set X • A ⊆ S  ≡  B ⊆ S)` and substitution  ⟩
          A ⊆ A ⇒ B ⊆ B ⇒ A = B
        ≡⟨ “Reflexivity of ⊆” and “Left-identity of ⇒” ⟩
          A = B








Theorem “Complement as set difference”: ~ A = 𝐔 - A
Proof:
  Using “Set Equality”:
    Subproof for `∀ e • e ∈ ~ A ≡ e ∈ (𝐔 - A)`:
      For any `e`:
          e ∈ ~ A ≡ e ∈ (𝐔 - A)
        ≡⟨ “Set difference” ⟩
          e ∈ ~ A ≡ e ∈ 𝐔 ∧ ¬ (e ∈ A)
        ≡⟨ “Complement” ⟩
          e ∈ ~ A ≡ e ∈ 𝐔 ∧ (e ∈ ~ A)
        ≡⟨ “Universal set” and “Identity of ∧” ⟩
          e ∈ ~ A ≡ (e ∈ ~ A)
        ≡⟨ “Reflexivity of ≡” ⟩
          true






Theorem “Complement as pseudocomplement”: ~ A = A ➩ {}
Proof:
  Using “Set Equality”:
    Subproof for `∀ e • e ∈ ~ A ≡ e ∈ (A ➩ {})`:
      For any `e`:
          e ∈ (A ➩ {})
        ≡⟨ “Membership in ➩” ⟩
          e ∈ A ⇒ e ∈ {}
        ≡⟨ “Empty set” ⟩
          e ∈ A ⇒ false
        ≡⟨ (3.74) ⟩
          ¬ (e ∈ A)
        ≡⟨ “Complement” ⟩
          e ∈ ~ A







Theorem “Antitonicity of ➩”:  A ⊆ B  ⇒  B ➩ C ⊆ A ➩ C
Proof:
  Assuming `A ⊆ B`:
    Using “Inclusion”:
      Subproof for `∀ e ❙ e ∈ (B ➩ C) • e ∈ (A ➩ C)`:
        For any `e` satisfying `e ∈ (B ➩ C)`:
            true
          ≡⟨ Assumption `e ∈ (B ➩ C)` ⟩
            e ∈ (B ➩ C)
          ≡⟨ “Membership in ➩” ⟩
            e ∈ B ⇒ e ∈ C
          ⇒⟨ “Antitonicity of ⇒” with “Casting” with Assumption `A ⊆ B` ⟩
            e ∈ A ⇒ e ∈ C
          ≡⟨ “Membership in ➩” ⟩
            e ∈ (A ➩ C)