Theorem “Domain of intersection”: Dom (R ∩ S) ⊆ Dom R ∩ Dom S
Proof:
  Using “Set inclusion”:
    Subproof for `∀ x • x ∈ Dom (R ∩ S) ⇒ x ∈ Dom R ∩ Dom S`:
      For any `x`:
           x ∈ Dom (R ∩ S) ⇒ x ∈ Dom R ∩ Dom S
         ≡⟨ “Definition of ⇒” ⟩
           x ∈ Dom (R ∩ S) ∧ x ∈ Dom R ∩ Dom S ≡ x ∈ Dom (R ∩ S)
         ≡⟨ “Golden rule” ⟩
           (x ∈ Dom (R ∩ S)) ∨ (x ∈ Dom R ∩ Dom S) ≡ x ∈ Dom R ∩ Dom S
         ≡⟨ “Intersection” ⟩
           (x ∈ Dom (R ∩ S)) ∨ (x ∈ Dom R ∧ x ∈ Dom S) ≡ x ∈ Dom R ∧ x ∈ Dom S
         ≡⟨ “Distributivity of ∨ over ∧” ⟩
           (x ∈ Dom (R ∩ S) ∨ x ∈ Dom R) ∧ (x ∈ Dom (R ∩ S) ∨ x ∈ Dom S) ≡ x ∈ Dom R ∧ x ∈ Dom S
         ≡⟨ “Membership in `Dom`” ⟩
           ((∃ y • x ⦗ R ∩ S ⦘ y) ∨ (∃ y • x ⦗ R ⦘ y)) ∧ ((∃ y • x ⦗ R ∩ S ⦘ y) ∨ (∃ y • x ⦗ S ⦘ y)) ≡ x ∈ Dom R ∧ x ∈ Dom S
         ≡⟨ “Relation intersection” ⟩
           ((∃ y • x ⦗ R ⦘ y ∧ x ⦗ S ⦘ y ) ∨ (∃ y • x ⦗ R ⦘ y)) ∧ ((∃ y • x ⦗ R ⦘ y ∧ x ⦗ S ⦘ y) ∨ (∃ y • x ⦗ S ⦘ y)) ≡ x ∈ Dom R ∧ x ∈ Dom S
         ≡⟨ “Distributivity of ∃ over ∨” ⟩
           (∃ y • (x ⦗ R ⦘ y ∧ x ⦗ S ⦘ y ) ∨ (x ⦗ R ⦘ y)) ∧ (∃ y • (x ⦗ R ⦘ y ∧ x ⦗ S ⦘ y) ∨ (x ⦗ S ⦘ y)) ≡ x ∈ Dom R ∧ x ∈ Dom S
         ≡⟨ “Distributivity of ∃ over ∨” ⟩
           (∃ y • (x ⦗ R ⦘ y ∧ x ⦗ S ⦘ y ) ∨ (x ⦗ R ⦘ y)) ∧ (∃ y • (x ⦗ R ⦘ y ∧ x ⦗ S ⦘ y) ∨ (x ⦗ S ⦘ y)) ≡ x ∈ Dom R ∧ x ∈ Dom S
         ≡⟨ “Absorption” ⟩
           (∃ y • (x ⦗ R ⦘ y)) ∧ (∃ y • (x ⦗ S ⦘ y)) ≡ x ∈ Dom R ∧ x ∈ Dom S
         ≡⟨ “Membership in `Dom`” ⟩
           x ∈ Dom R ∧ x ∈ Dom S ≡ x ∈ Dom R ∧ x ∈ Dom S
         ≡⟨ “Reflexivity of ≡” ⟩
           true