Lemma “Reflexivity of ⊆”: R = S  ⇒  R ⊆ S
Proof:
  Assuming `R = S`:
      R ⊆ S
    ≡⟨ Assumption `R = S`⟩
      S ⊆ S
    ≡⟨“Reflexivity of ⊆”⟩
      true


Theorem “Mutual inclusion”: R = S  ≡  R ⊆ S ∧ S ⊆ R
Proof:
  Using “Mutual implication”:
    Subproof for `R = S  ⇒  R ⊆ S ∧ S ⊆ R`:
      Assuming `R = S`:
          R ⊆ S ∧ S ⊆ R
        ≡⟨ Assumption `R = S`⟩
          S ⊆ S ∧ S ⊆ S
        ≡⟨“Idempotency of ∧”⟩
          S ⊆ S
        ≡⟨“Reflexivity of ⊆”⟩
          true
    Subproof for `R ⊆ S ∧ S ⊆ R ⇒ R = S`:
        R ⊆ S ∧ S ⊆ R ⇒ R = S
      ≡⟨“Shunting”⟩
        R ⊆ S ⇒ S ⊆ R ⇒ R = S
      ≡⟨“Antisymmetry of ⊆”⟩
        true



Theorem “Indirect Relation Equality”
        “Indirect Relation Equality from below”:
    Q = R  ≡  (∀ S • S ⊆ Q  ≡  S ⊆ R)
Proof:
  Using “Mutual implication”:
    Subproof for `Q = R  ⇒  (∀ S • S ⊆ Q  ≡  S ⊆ R)`:
      Assuming `Q = R`:
          (∀ S • S ⊆ Q  ≡  S ⊆ R)
        ≡⟨ Assumption `Q = R`⟩
          (∀ S • S ⊆ R  ≡  S ⊆ R)
        ≡⟨“Reflexivity of ≡”⟩
          (∀ S • true)
        ≡⟨“True ∀ body”⟩
          true
    Subproof for `(∀ S • S ⊆ Q  ≡  S ⊆ R) ⇒ Q = R`:
      Assuming `(∀ S • S ⊆ Q  ≡  S ⊆ R)`:
          Q = R
        ≡⟨“Left-identity of ⇒”⟩
          true ⇒ Q = R
        ≡⟨“Reflexivity of ⊆”⟩
          R ⊆ R ⇒ Q = R
        ≡⟨ Assumption `(∀ S • S ⊆ Q  ≡  S ⊆ R)`⟩
          R ⊆ Q ⇒ Q = R
        ⇐⟨“Antisymmetry of ⊆”⟩
          Q ⊆ R
        ≡⟨ Assumption `(∀ S • S ⊆ Q  ≡  S ⊆ R)`⟩
          Q ⊆ Q
        ≡⟨“Reflexivity of ⊆”⟩
          true




Theorem “Indirect Relation Inclusion”
        “Indirect Relation Inclusion from above”:
    Q ⊆ R  ≡  (∀ S • R ⊆ S  ⇒  Q ⊆ S)
Proof:
  Using “Mutual implication”:
    Subproof for `Q ⊆ R  ⇒  (∀ S • R ⊆ S  ⇒  Q ⊆ S)`:
      Assuming `Q ⊆ R `:
        For any `S`:
            R ⊆ S  ⇒  Q ⊆ S
          ≡⟨“Left-identity of ⇒”⟩
            true ⇒ R ⊆ S  ⇒  Q ⊆ S
          ≡⟨ Assumption `Q ⊆ R`⟩
            Q ⊆ R ⇒ R ⊆ S  ⇒  Q ⊆ S
          ≡⟨“Transitivity of ⊆”⟩
            true
    Subproof for `(∀ S • R ⊆ S  ⇒  Q ⊆ S) ⇒ Q ⊆ R`:
        Assuming `(∀ S • R ⊆ S  ⇒  Q ⊆ S)`:
            Q ⊆ R
          ⇐⟨ Assumption `(∀ S • R ⊆ S  ⇒  Q ⊆ S)`⟩
            R ⊆ R
          ≡⟨“Reflexivity of ⊆”⟩
            true



Lemma “Cancellation of ˘”:
    R ˘ = S ˘  ≡  R = S
Proof:
  Using “Mutual implication”:
    Subproof for `R ˘ = S ˘  ⇒  R = S`:
      Assuming `R ˘ = S ˘ `:
          R = S
        ≡⟨“Self-inverse of ˘”⟩
          R ˘ ˘ = S
        ≡⟨ Assumption `R ˘ = S ˘ `⟩
          S ˘ ˘ = S
        ≡⟨“Self-inverse of ˘”⟩
          S  = S
        ≡⟨“Reflexivity of =”⟩
          true
    Subproof for `R = S   ⇒  R ˘ = S ˘`:
      Assuming `R = S`:
          R ˘ = S ˘
        ≡⟨ Assumption `R = S`⟩
          S ˘  = S ˘
        ≡⟨“Reflexivity of =”⟩
          true







Theorem “Isotonicity of ˘”:  R ⊆ S  ≡  R ˘ ⊆ S ˘
Proof:
  Using “Mutual implication”:
    Subproof for `R ⊆ S  ⇒  R ˘ ⊆ S ˘ `:
        R ⊆ S  ⇒  R ˘ ⊆ S ˘
      ≡⟨“Monotonicity of ˘”⟩
        true
    Subproof for `R ˘ ⊆ S ˘  ⇒  R ⊆ S `:
      Assuming `R ˘ ⊆ S ˘ `:
          R ⊆ S
        ≡⟨“Self-inverse of ˘”⟩
          R ˘ ˘ ⊆ S ˘ ˘
        ⇐⟨“Monotonicity of ˘”⟩
          R ˘  ⊆ S ˘
        ≡⟨ Assumption `R ˘ ⊆ S ˘ `⟩
          true




Lemma “Definition of symmetry”:
    is-symmetric R   ≡   R ˘ = R
Proof:
    is-symmetric R   ≡   R ˘ = R
  ≡⟨“Definition of symmetry”⟩
    R ˘ ⊆ R   ≡   R ˘ = R
  ≡⟨“Mutual inclusion”⟩
    R ˘ ⊆ R   ≡   R ˘ ⊆ R ∧ R  ⊆ R ˘
  ≡⟨“Definition of ⇒”⟩
    R ˘ ⊆ R ⇒ R  ⊆ R ˘
  ≡⟨“Self-inverse of ˘”⟩
    R ˘ ⊆ R ⇒ R ˘ ˘  ⊆ R ˘
  ≡⟨“Monotonicity of ˘”⟩
    true




 Theorem “Reflexivity of converse”:
    is-reflexive R ≡ is-reflexive (R ˘)
Proof:
    is-reflexive R ≡ is-reflexive (R ˘)
  ≡⟨“Definition of reflexivity”⟩
    Id ⊆ R ≡ Id ⊆ R ˘
  ≡⟨“Self-inverse of ˘”⟩
    Id ˘ ˘ ⊆ R ˘ ˘ ≡ Id  ˘ ˘ ⊆ R ˘ ˘ ˘
  ≡⟨“Isotonicity of ˘”⟩
    Id ˘ ⊆ R ˘ ≡ Id  ˘  ⊆ R  ˘ ˘
  ≡⟨“Converse of `Id`”⟩
    Id ⊆ R ˘ ≡ Id  ˘  ⊆ R  ˘ ˘
  ≡⟨“Isotonicity of ˘”⟩
    true




Theorem “Reflexivity of ⨾”:
    is-reflexive R ⇒ is-reflexive S ⇒ is-reflexive (R ⨾ S)
Proof:
      is-reflexive R ⇒ is-reflexive S ⇒ is-reflexive (R ⨾ S)
    ≡⟨“Definition of reflexivity”⟩
      Id ⊆ R ⇒ Id ⊆ S ⇒ Id ⊆ (R ⨾ S)
    ≡⟨“Identity of ⨾”⟩
      Id ⊆ R ⇒ Id ⨾ Id ⊆ S ⇒ Id ⨾ Id ⨾ Id  ⊆ (R ⨾ S)
    ≡⟨“Monotonicity of ⨾”⟩
      true





Theorem “Symmetry of converse”:
    is-symmetric R ≡ is-symmetric (R ˘)
Proof:
    is-symmetric R ≡ is-symmetric (R ˘)
  ≡⟨“Definition of symmetry”⟩
    R ˘ ⊆ R ≡ R ˘ ˘ ⊆ R ˘
  ≡⟨“Self-inverse of ˘”⟩
    R ˘ ⊆ R ≡ R ⊆ R ˘
  ≡⟨“Isotonicity of ˘”⟩
    R ˘ ˘ ⊆ R ˘ ≡ R ⊆ R ˘
  ≡⟨“Self-inverse of ˘”⟩
    R  ⊆ R ˘ ≡ R ⊆ R ˘
  ≡⟨“Reflexivity of ≡”⟩
    true


Theorem “Symmetry of converse”:
    is-symmetric R ≡ is-symmetric (R ˘)
Proof:
    is-symmetric R ≡ is-symmetric (R ˘)
  ≡⟨“Definition of symmetry”⟩
    R ˘ ⊆ R ≡ R ˘ ˘ ⊆ R ˘
  ≡⟨“Self-inverse of ˘”⟩
    R ˘ ⊆ R ≡ R ⊆ R ˘
  ≡⟨“Isotonicity of ˘”⟩
    R ˘ ˘ ⊆ R ˘ ≡ R ⊆ R ˘
  ≡⟨“Self-inverse of ˘”⟩
    R  ⊆ R ˘ ≡ R ⊆ R ˘
  ≡⟨“Reflexivity of ≡”⟩
    true




Theorem “Symmetry of ∩”: Q ∩ R  ⊆  R ∩ Q
Proof:
    Q ∩ R  ⊆  R ∩ Q
  ≡⟨“Characterisation of ∩”⟩
    Q ∩ R  ⊆  R ∧ Q ∩ R  ⊆  Q
  ≡⟨“Weakening for ∩”⟩
    true


 Corollary “Symmetry of ∩”: Q ∩ R  =  R ∩ Q
Proof:
    Q ∩ R  =  R ∩ Q
  ≡⟨“Mutual inclusion”⟩
    (Q ∩ R  ⊆  R ∩ Q) ∧ (R ∩ Q ⊆ Q ∩ R)
  ≡⟨“Characterisation of ∩”⟩
    (Q ∩ R  ⊆  R ∧ Q ∩ R  ⊆  Q) ∧ (R ∩ Q ⊆ Q ∧ R ∩ Q ⊆ R)
  ≡⟨“Weakening for ∩”⟩
    true ∧ true
  ≡⟨“Idempotency of ∧”⟩
    true


  Theorem “Associativity of ∩”: (Q ∩ R) ∩ S  ⊆  Q ∩ (R ∩ S)
Proof:
    (Q ∩ R) ∩ S  ⊆  Q ∩ (R ∩ S)
  ≡⟨“Characterisation of ∩”⟩
    (Q ∩ R) ∩ S  ⊆  Q ∧ (Q ∩ R) ∩ S ⊆ (R ∩ S)
  ≡⟨“Characterisation of ∩”⟩
    (Q ∩ R) ∩ S  ⊆  Q ∧ (Q ∩ R) ∩ S ⊆ R ∧ (Q ∩ R) ∩ S ⊆ S
  ≡⟨“Characterisation of ∩”⟩
    ((Q ∩ R) ∩ S  ⊆  Q ∩ R) ∧ (Q ∩ R) ∩ S ⊆ S
  ≡⟨“Weakening for ∩”⟩
    true



Corollary “Associativity of ∩”: (Q ∩ R) ∩ S  =  Q ∩ (R ∩ S)
Proof:
    (Q ∩ R) ∩ S  =  Q ∩ (R ∩ S)
  ≡⟨“Mutual inclusion”⟩
    ((Q ∩ R) ∩ S  ⊆  Q ∩ (R ∩ S)) ∧ (Q ∩ (R ∩ S) ⊆ (Q ∩ R) ∩ S)
  ≡⟨“Associativity of ∩”⟩
    true ∧ true
  ≡⟨“Idempotency of ∧”⟩
    true




  Theorem “Idempotency of ∩”: R ∩ R = R
Proof:
    R ∩ R = R
  ≡⟨“Mutual inclusion”⟩
    R ∩ R ⊆ R ∧ R ⊆  R ∩ R
  ≡⟨“Characterisation of ∩”⟩
    R ∩ R ⊆ R ∧ R ⊆ R ∧ R ⊆ R
  ≡⟨“Reflexivity of ⊆”, “Idempotency of ∧”, “Identity of ∧”⟩
    R ∩ R ⊆ R
  ≡⟨“Idempotency of ∧”⟩
    R ∩ R ⊆ R ∧ R ∩ R ⊆ R
  ≡⟨“Weakening for ∩”⟩
    true




Theorem “Monotonicity of ∩”: Q ⊆ R  ⇒  Q ∩ S ⊆ R ∩ S
Proof:
    Q ⊆ R  ⇒  Q ∩ S ⊆ R ∩ S
  ≡⟨“Characterisation of ∩”⟩
    Q ⊆ R  ⇒  (Q ∩ S ⊆ R) ∧  (Q ∩ S ⊆ S)
  ≡⟨“Identity of ∧”⟩
    Q ⊆ R  ⇒  (Q ∩ S ⊆ R)  ∧ (Q ∩ S ⊆ S)  ∧ true
  ≡⟨“Weakening for ∩”⟩
    Q ⊆ R  ⇒  (Q ∩ S ⊆ R)  ∧ (Q ∩ S ⊆ S)  ∧ (Q ∩ S ⊆ Q)  ∧ (Q ∩ S ⊆ S)
  ≡⟨“Idempotency of ∧”⟩
    Q ⊆ R  ⇒  (Q ∩ S ⊆ R)  ∧ (Q ∩ S ⊆ S) ∧ (Q ∩ S ⊆ Q)
  ≡⟨“Weakening for ∩”⟩
    Q ⊆ R  ⇒  (Q ∩ S ⊆ R)  ∧ true
  ≡⟨“Identity of ∧”⟩
    Q ⊆ R  ⇒  (Q ∩ S ⊆ R)
  ⇐⟨“Transitivity of ⊆”⟩
    Q ∩ S ⊆ Q
  ≡⟨“Idempotency of ∧” and “Weakening for ∩”⟩
    true




 Theorem “Inclusion via ∩”: Q ⊆ R  ≡  Q ∩ R = Q
Proof:
     Q ∩ R = Q
  ≡⟨“Mutual inclusion”⟩
     Q ∩ R ⊆ Q ∧ Q ⊆ Q ∩ R
  ≡⟨“Identity of ∧”⟩
     Q ∩ R ⊆ Q ∧ Q ⊆ Q ∩ R ∧ true
  ≡⟨“Weakening for ∩”⟩
     Q ∩ R ⊆ Q ∧ Q ⊆ Q ∩ R ∧ Q ∩ R ⊆ Q ∧ Q ∩ R ⊆ R
  ≡⟨“Idempotency of ∧”⟩
     Q ∩ R ⊆ Q ∧ Q ⊆ Q ∩ R ∧ Q ∩ R ⊆ R
  ≡⟨“Weakening for ∩”⟩
     true ∧ Q ⊆ Q ∩ R
  ≡⟨“Identity of ∧”⟩
     Q ⊆ Q ∩ R
  ≡⟨“Characterisation of ∩”⟩
     Q ⊆ Q ∧ Q ⊆ R
  ≡⟨“Reflexivity of ⊆”, “Identity of ∧”⟩
     Q ⊆ R



Theorem “Converse of ∩”:     (R ∩ S) ˘  ⊆  R ˘ ∩ S ˘
Proof:
    (R ∩ S) ˘  ⊆  R ˘ ∩ S ˘
  ≡⟨“Characterisation of ∩”⟩
    (R ∩ S) ˘  ⊆  R ˘ ∧  (R ∩ S) ˘  ⊆  S ˘
  ≡⟨“Isotonicity of ˘”⟩
    (R ∩ S) ⊆  R  ∧  (R ∩ S)  ⊆  S
  ≡⟨“Weakening for ∩”⟩
    true







Theorem “Converse of ∩”:     (R ∩ S) ˘  =  R ˘ ∩ S ˘
Proof:
    (R ∩ S) ˘  =  R ˘ ∩ S ˘
  ≡⟨“Mutual inclusion”⟩
    (R ∩ S) ˘  ⊆  R ˘ ∩ S ˘ ∧ R ˘ ∩ S ˘ ⊆ (R ∩ S) ˘
  ≡⟨“Converse of ∩”, “Identity of ∧”⟩
     R ˘ ∩ S ˘ ⊆ (R ∩ S) ˘
  ≡⟨“Isotonicity of ˘”⟩
     (R ˘ ∩ S ˘) ˘ ⊆ (R ∩ S) ˘ ˘
  ≡⟨“Self-inverse of ˘”⟩
     (R ˘ ∩ S ˘) ˘ ⊆ (R ∩ S)
  ≡⟨“Self-inverse of ˘”⟩
     (R ˘ ∩ S ˘) ˘ ⊆ (R ˘ ˘ ∩ S ˘ ˘)
  ≡⟨“Converse of ∩”⟩
    true



Theorem “Sub-distributivity of ⨾ over ∩”:
    Q ⨾ (R ∩ S)  ⊆  Q ⨾ R  ∩  Q ⨾ S
Proof:
    Q ⨾ (R ∩ S)
  =⟨“Idempotency of ∩”⟩
    (Q ⨾ (R ∩ S)) ∩ (Q ⨾ (R ∩ S))
  ⊆⟨“Monotonicity of ∩” with “Monotonicity of ⨾” with “Weakening for ∩”⟩
    (Q ⨾ (R ∩ S)) ∩  Q ⨾ S
  ⊆⟨“Monotonicity of ∩” with “Monotonicity of ⨾” with “Weakening for ∩”⟩
    (Q ⨾ R) ∩  Q ⨾ S








Theorem “Antisymmetry of converse”:  is-antisymmetric R  ≡  is-antisymmetric (R ˘)
Proof:
    is-antisymmetric R  ≡  is-antisymmetric (R ˘)
  ≡⟨“Definition of antisymmetry”⟩
    R ∩ R ˘ ⊆ Id  ≡  R ˘ ∩ R ˘ ˘ ⊆ Id
  ≡⟨“Self-inverse of ˘”⟩
    R ∩ R ˘ ⊆ Id  ≡  R ˘ ∩ R ⊆ Id
  ≡⟨“Symmetry of ∩”⟩
    R ˘ ∩ R ⊆ Id ≡  R ˘ ∩ R ⊆ Id
  ≡⟨“Reflexivity of ≡”⟩
    true






Theorem “Converse of an order”:  is-order E  ≡  is-order (E ˘)
Proof:
    is-order E  ≡  is-order (E ˘)
  ≡⟨“Definition of ordering”⟩
    is-reflexive E ∧ is-antisymmetric E ∧ is-transitive E ≡ is-reflexive (E ˘)  ∧ is-antisymmetric (E ˘)  ∧ is-transitive (E ˘)
  ≡⟨“Reflexivity of converse”, “Antisymmetry of converse”⟩
    is-reflexive (E ˘) ∧ is-antisymmetric (E ˘) ∧ is-transitive E ≡ is-reflexive (E ˘)  ∧ is-antisymmetric (E ˘)  ∧ is-transitive (E ˘)
  ≡⟨“Definition of transitivity”⟩
    is-reflexive (E ˘) ∧ is-antisymmetric (E ˘) ∧ (E ⨾ E ⊆ E) ≡ is-reflexive (E ˘)  ∧ is-antisymmetric (E ˘)  ∧ (E ˘ ⨾ E ˘ ⊆ E ˘)
  ≡⟨“Converse of ⨾”⟩
    is-reflexive (E ˘) ∧ is-antisymmetric (E ˘) ∧ (E ⨾ E ⊆ E) ≡ is-reflexive (E ˘)  ∧ is-antisymmetric (E ˘)  ∧ ((E ⨾ E) ˘ ⊆ E ˘)
  ≡⟨“Isotonicity of ˘”⟩
    is-reflexive (E ˘) ∧ is-antisymmetric (E ˘) ∧ (E ⨾ E ⊆ E) ≡ is-reflexive (E ˘)  ∧ is-antisymmetric (E ˘)  ∧ ((E ⨾ E) ⊆ E)
  ≡⟨“Reflexivity of ≡”⟩
    true