Theorem “Relationship via 𝕀”: x ⦗ 𝕀 B ⦘ y  ≡  x = y ∈ B
Proof:
    x ⦗ 𝕀 B ⦘ y
  ≡⟨ “Definition of 𝕀” ⟩
    x ⦗ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⦘ y
  ≡⟨ “Infix relationship” ⟩
    ⟨ x , y ⟩ ∈ { z ❙ z ∈ B • ⟨ z , z ⟩ }
  ≡⟨ “Set membership” ⟩
    ∃ z ❙ z ∈ B • ⟨ x , y ⟩ = ⟨ z , z ⟩
  ≡⟨ “Pair equality” ⟩
    ∃ z ❙ z ∈ B • x = z ∧ y = z
  ≡⟨ “Trading for ∃” ⟩
    ∃ z ❙ y = z • x = z ∧ z ∈ B
  ≡⟨ “One-point rule for ∃”, Substitution ⟩
    x = y ∈ B

Theorem “Intersection of 𝕀 relations”: 𝕀 B ∩ 𝕀 C = 𝕀 (B ∩ C)
Proof:
    𝕀 B ∩ 𝕀 C = 𝕀 (B ∩ C)
  ≡ ⟨ “Relation extensionality” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ∩ 𝕀 C ⦘ y ≡ x ⦗ 𝕀 (B ∩ C) ⦘ y
  ≡ ⟨ “Relationship via 𝕀” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ∩ 𝕀 C ⦘ y ≡ x = y ∧ y ∈ (B ∩ C)
  ≡ ⟨ “Relation intersection” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ x ⦗ 𝕀 C ⦘ y ≡ x = y ∈ (B ∩ C)
  ≡ ⟨ “Intersection” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ x ⦗ 𝕀 C ⦘ y ≡ x = y ∧ (y ∈ B ∧ y ∈ C)
  ≡ ⟨ Subproof:
        For any `x`, `y`:
            x ⦗ 𝕀 B ⦘ y ∧ x ⦗ 𝕀 C ⦘ y
          ≡ ⟨“Relationship via 𝕀”⟩
            x = y ∧ y ∈ B ∧ x = y ∧ y ∈ C
          ≡ ⟨ “Idempotency of ∧” ⟩
             x = y ∧ (y ∈ B ∧ y ∈ C)
    ⟩
    true


Theorem “Union of 𝕀 relations”: 𝕀 B ∪ 𝕀 C = 𝕀 (B ∪ C)
Proof:
    𝕀 B ∪ 𝕀 C = 𝕀 (B ∪ C)
  ≡ ⟨ “Relation extensionality” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ∪ 𝕀 C ⦘ y ≡ x ⦗ 𝕀 (B ∪ C) ⦘ y
  ≡ ⟨ “Relationship via 𝕀” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ∪ 𝕀 C ⦘ y ≡ x = y ∧ y ∈ (B ∪ C)
  ≡ ⟨ “Relation union” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∨ x ⦗ 𝕀 C ⦘ y ≡ x = y ∈ (B ∪ C)
  ≡ ⟨ “Union” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∨ x ⦗ 𝕀 C ⦘ y ≡ x = y ∧ (y ∈ B ∨ y ∈ C)
  ≡ ⟨ Subproof:
        For any `x`, `y`:
            x ⦗ 𝕀 B ⦘ y ∨ x ⦗ 𝕀 C ⦘ y
          ≡ ⟨“Relationship via 𝕀”⟩
            (x = y ∧ y ∈ B) ∨ (x = y ∧ y ∈ C)
          ≡ ⟨ “Distributivity of ∧ over ∨” ⟩
            x = y ∧ (y ∈ B ∨ y ∈ C)
    ⟩
    true

Theorem “Difference of 𝕀 relations”: 𝕀 B - 𝕀 C = 𝕀 (B - C)
Proof:
    𝕀 B - 𝕀 C = 𝕀 (B - C)
  ≡ ⟨ “Relation extensionality” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B - 𝕀 C ⦘ y ≡ x ⦗ 𝕀 (B - C) ⦘ y
  ≡ ⟨ “Relationship via 𝕀” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B - 𝕀 C ⦘ y ≡ x = y ∧ y ∈ (B - C)
  ≡ ⟨ “Relation difference” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ ¬ ( x ⦗ 𝕀 C ⦘ y ) ≡ x = y ∈ (B - C)
  ≡ ⟨ “Set difference” ⟩
    ∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ∧ ¬ ( x ⦗ 𝕀 C ⦘ y ) ≡ x = y ∧ (y ∈ B ∧ ¬ (y ∈ C))
  ≡ ⟨ Subproof:
        For any `x`, `y`:
            x ⦗ 𝕀 B ⦘ y ∧ ¬ ( x ⦗ 𝕀 C ⦘ y )
          ≡ ⟨“Relationship via 𝕀”⟩
            (x = y ∧ y ∈ B) ∧ ¬ (x = y ∧ y ∈ C)
          ≡ ⟨“De Morgan”, “Distributivity of ∧ over ∨”, “Contradiction”, “Identity of ∨” ⟩
            x = y ∧ (y ∈ B ∧ ¬ (y ∈ C))
    ⟩
    true

Theorem “Set complement as difference”: ~ B = 𝐔 - B
Proof:
    ~ B = 𝐔 - B
  ≡ ⟨“Set extensionality”⟩
    ∀ e • e ∈ ~ B ≡ e ∈ 𝐔 - B
  ≡ ⟨“Set difference”, “Universal set”, “Identity of ∧”⟩
    ∀ e • e ∈ ~ B ≡ ¬ (e ∈ B)
  ≡ ⟨“Complement”⟩
    ∀ e • true — This is “True ∀ body”


Theorem “Intersection of 𝕀 and ×”: 𝕀 B ∩ (C × D) = 𝕀 (B ∩ C ∩ D)
Proof:
  Using “Relation extensionality”:
    For any `x`, `y`:
         x ⦗ 𝕀 B ∩ (C × D) ⦘ y
      ≡ ⟨ “Relation intersection” ⟩
         x ⦗ 𝕀 B ⦘ y ∧ x ⦗ (C × D) ⦘ y
      ≡ ⟨ “Relationship via 𝕀”, “Infix relationship” ⟩
         x = y ∧ y ∈ B ∧ ⟨ x , y ⟩ ∈ (C × D)
      ≡ ⟨ “Membership in ×” ⟩
         x = y ∧ y ∈ B ∧ x ∈ C ∧ y ∈ D
      ≡ ⟨ Substitution ⟩
         x = y ∧ (y ∈ B ∧ z ∈ C ∧ y ∈ D)[z ≔ x]
      ≡ ⟨ “Replacement”, Substitution ⟩
         x = y ∧ (y ∈ B ∧ y ∈ C ∧ y ∈ D)
      ≡ ⟨ “Intersection” ⟩
         x = y ∧ (y ∈ B ∩ C ∩ D)
      ≡ ⟨ “Relationship via 𝕀” ⟩
         x ⦗ 𝕀 (B ∩ C ∩ D) ⦘ y


Theorem “Difference of 𝕀 and ×”: 𝕀 B - (C × D) = 𝕀 (B - (C ∩ D))
Proof:
  Using “Relation extensionality”:
    For any `x`, `y`:
        x ⦗ 𝕀 B - (C × D) ⦘ y
      ≡ ⟨“Relation difference”⟩
        (( x ⦗ 𝕀 B ⦘ y ) ∧ ¬ ( x ⦗ (C × D) ⦘ y ))
      ≡ ⟨“Infix relationship”, “Relationship via 𝕀”, “Membership in ×”⟩
         x = y ∧ y ∈ B ∧ ¬ (x ∈ C ∧ y ∈ D)
      ≡ ⟨Substitution⟩
         x = y ∧ (y ∈ B ∧ ¬ (z ∈ C ∧ y ∈ D))[z ≔ x]
      ≡ ⟨“Replacement”, Substitution⟩
         x = y ∧ y ∈ B ∧ ¬ (y ∈ C ∧ y ∈ D)
      ≡ ⟨“Intersection”⟩
         x = y ∧ y ∈ B ∧ ¬ (y ∈ C ∩ D)
      ≡ ⟨“Relationship via 𝕀”, “Set difference”⟩
         x ⦗ 𝕀 (B - (C ∩ D)) ⦘ y


Theorem “Isotonicity of 𝕀”:  B ⊆ C  ≡  𝕀 B ⊆ 𝕀 C
Proof:
    𝕀 B ⊆ 𝕀 C
  ≡ ⟨ “Set inclusion” ⟩
    ∀ e ❙ e ∈ 𝕀 B • e ∈ 𝕀 C
  ≡ ⟨ “Definition of 𝕀”, “Trading for ∀” ⟩
    ∀ e • e ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⇒ e ∈ { x ❙ x ∈ C • ⟨ x , x ⟩ }
  ≡ ⟨ Subproof for `e ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⇒ e ∈ { x ❙ x ∈ C • ⟨ x , x ⟩ } ≡ ∀ e • e ∈ B ⇒ e ∈ C`:
        e ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ } ⇒ e ∈ { x ❙ x ∈ C • ⟨ x , x ⟩ }
      ≡ ⟨ ? ⟩
        e ∈ B ⇒ e ∈ C
    ⟩
    ∀ e • e ∈ B ⇒ e ∈ C
  ≡ ⟨“Trading for ∀”, “Set inclusion”⟩
    B ⊆ C