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


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



Theorem “Set complement as difference”: ~ B = 𝐔 - B
Proof:
  Using “Set extensionality”:
    Subproof for `∀ x • x ∈ ~ B ≡ x ∈ (𝐔 - B)`:
      For any `x`:
          x ∈ ~ B
        ≡⟨ “Complement” ⟩
          ¬ (x ∈ B)
        ≡⟨ “Identity of ∧” ⟩
          ¬ (x ∈ B) ∧ true
        ≡⟨ “Universal set” ⟩
          ¬ (x ∈ B) ∧ x ∈ 𝐔
        ≡⟨ “Set difference” ⟩
          x ∈ 𝐔 - B



Theorem “Difference of 𝕀 relations”: 𝕀 (~ B) = 𝕀 𝐔 - 𝕀 B
Proof:
  Using “Relation extensionality”:
    Subproof for `∀ x • ∀ y • x ⦗ 𝕀 (~ B) ⦘ y ≡ x ⦗ 𝕀 𝐔 - 𝕀 B ⦘ y`:
      For any `x`, `y`:
          x ⦗ 𝕀 (~ B) ⦘ y
        ≡⟨ “Set complement as difference” ⟩
          x ⦗ 𝕀 (𝐔 - B) ⦘ y
        ≡⟨ “Difference of 𝕀 relations” ⟩
          x ⦗ 𝕀 𝐔 - 𝕀 B ⦘ y