Theorem “Relation inclusion”:
    R ⊆ S  ≡  (∀ x • ∀ y ❙ x ⦗ R ⦘ y  •  x ⦗ S ⦘ y)
Proof:
    R ⊆ S  ≡  (∀ x • ∀ y ❙ x ⦗ R ⦘ y  •  x ⦗ S ⦘ y)
  =⟨ “Trading for ∀”⟩
    R ⊆ S  ≡  (∀ x • ∀ y • x ⦗ R ⦘ y  ⇒  x ⦗ S ⦘ y)
  =⟨ “Relation inclusion”⟩
    true



Theorem “Relation inclusion”:
    R ⊆ S  ≡  (∀ x, y ❙ x ⦗ R ⦘ y  •  x ⦗ S ⦘ y)
Proof:
    R ⊆ S  ≡  (∀ x, y ❙ x ⦗ R ⦘ y  •  x ⦗ S ⦘ y)
  =⟨ “Nesting for ∀”⟩
    R ⊆ S  ≡  (∀ x • ∀ y ❙ x ⦗ R ⦘ y  •  x ⦗ S ⦘ y)
  =⟨ “Relation inclusion”⟩
    true


Theorem “Empty relation”: a ⦗ {} ⦘ b  ≡ false
Proof:
    a ⦗ {} ⦘ b
  =⟨ “Definition of `_⦗_⦘_`”⟩
    ⟨ a , b ⟩ ∈ {}
  =⟨ “Empty set” ⟩
    false

Lemma “Singleton relation”:
    a₁ ⦗ { ⟨ a₂ , b₂ ⟩ } ⦘ b₁  ≡  a₁ = a₂ ∧ b₁ = b₂
Proof:
    a₁ ⦗ { ⟨ a₂ , b₂ ⟩ } ⦘ b₁  ≡  a₁ = a₂ ∧ b₁ = b₂
  =⟨ “Definition of `_⦗_⦘_`”⟩
    ⟨ a₁, b₁ ⟩ ∈ { ⟨ a₂ , b₂ ⟩ }   ≡  a₁ = a₂ ∧ b₁ = b₂
  =⟨ “Pair equality”⟩
    ⟨ a₁, b₁ ⟩ ∈ { ⟨ a₂ , b₂ ⟩ }   ≡  ⟨a₁, b₁⟩ = ⟨ a₂, b₂⟩
  =⟨ “Singleton set membership”⟩
    ⟨ a₁, b₁ ⟩ ∈ { ⟨ a₂ , b₂ ⟩ }   ≡  ⟨a₁, b₁⟩ ∈ {⟨ a₂, b₂⟩}
  =⟨ “Reflexivity of ≡”⟩
    true

Lemma “Singleton relation inclusion”:
    { ⟨ a , b ⟩ } ⊆ R  ≡  a ⦗ R ⦘ b
Proof:
    a ⦗ R ⦘ b
  =⟨ “Definition of `_⦗_⦘_`”⟩
    ⟨ a, b ⟩ ∈ R
  =⟨ “Singleton set inclusion”⟩
    { ⟨ a , b ⟩ } ⊆ R


Theorem “Relation complement”: a ⦗ ~ R ⦘ b  ≡  ¬ (a ⦗ R ⦘ b)
Proof:
    a ⦗ ~ R ⦘ b
  =⟨ “Definition of `_⦗_⦘_`”⟩
    ⟨ a, b ⟩ ∈ ~ R
  =⟨ “Complement”⟩
    ¬ (⟨ a, b ⟩ ∈ R)
  =⟨ “Definition of `_⦗_⦘_`”⟩
    ¬ (a ⦗ R ⦘ b)


Theorem “Relation union”:
    a ⦗ R ∪ S ⦘ b  ≡  a ⦗ R ⦘ b  ∨  a ⦗ S ⦘ b
Proof:
    a ⦗ R ∪ S ⦘ b
  =⟨ “Definition of `_⦗_⦘_`”⟩
    ⟨ a, b ⟩ ∈ R ∪ S
  =⟨ “Union”⟩
    ⟨ a, b ⟩ ∈ R ∨ ⟨ a, b ⟩ ∈ S
  =⟨ “Definition of `_⦗_⦘_`”⟩
    a ⦗ R ⦘ b  ∨  a ⦗ S ⦘ b



Theorem “Relation intersection”: a ⦗ R ∩ S ⦘ b  ≡  a ⦗ R ⦘ b ∧ a ⦗ S ⦘ b
Proof:
    a ⦗ R ∩ S ⦘ b
  =⟨ “Definition of `_⦗_⦘_`”⟩
    ⟨ a, b⟩ ∈ R ∩ S
  =⟨ “Intersection”⟩
    ⟨ a, b⟩ ∈ R ∧ ⟨ a, b⟩ ∈ S
  =⟨ “Definition of `_⦗_⦘_`”⟩
    a ⦗ R ⦘ b ∧ a ⦗ S ⦘ b


Theorem “Relation difference”: a ⦗ R - S ⦘ b  ≡  a ⦗ R ⦘ b ∧ ¬ (a ⦗ S ⦘ b)
Proof:
    a ⦗ R - S ⦘ b
  =⟨ “Definition of `_⦗_⦘_`”⟩
    ⟨ a, b ⟩ ∈ R - S
  =⟨ “Set difference”⟩
    ⟨ a, b ⟩ ∈ R ∧ ¬ (⟨ a, b ⟩ ∈ S)
  =⟨ “Definition of `_⦗_⦘_`”⟩
    a ⦗ R ⦘ b ∧ ¬ (a ⦗ S ⦘ b)