Theorem “Weakening for ∩”: Q ∩ R ⊆ Q  ∧  Q ∩ R ⊆ R
Proof:
    By “Characterisation of ∩”, “Reflexivity of ⊆”

Theorem “Symmetry of ∩”: Q ∩ R  ⊆  R ∩ Q
Proof:
    By “Characterisation of ∩”, “Reflexivity of ⊆”

Corollary “Symmetry of ∩”: Q ∩ R  =  R ∩ Q
Proof:
    Q ∩ R  =  R ∩ Q
  =⟨ “Mutual inclusion” ⟩
    Q ∩ R ⊆ R ∩ Q ∧ R ∩ Q ⊆ Q ∩ R
  =⟨ “Symmetry of ∩”, “Identity of ∧” ⟩
    R ∩ Q ⊆ Q ∩ R
  =⟨ “Characterisation of ∩” ⟩
    R ∩ Q ⊆ Q ∧  R ∩ Q ⊆ R
  =⟨ “Characterisation of ∩” ⟩
    R ∩ Q ⊆ R ∩ Q
  =⟨ “Reflexivity of ⊆” ⟩
    true

Theorem “Associativity of ∩”: (Q ∩ R) ∩ S  ⊆  Q ∩ (R ∩ S)
Proof:
   By “Characterisation of ∩”, “Reflexivity of ⊆”

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 ∩”, “Identity of ∧” ⟩
    Q ∩ (R ∩ S) ⊆ (Q ∩ R) ∩ S
  =⟨ “Characterisation of ∩” ⟩
    Q ∩ (R ∩ S) ⊆ Q ∩ (R ∩ S)
  =⟨ “Reflexivity 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 ⊆”, “Identity of ∧” ⟩
    R ∩ R ⊆ R
  =⟨ “Characterisation of ∩” ⟩
    R ∩ R ⊆ R
  =⟨ “Idempotency of ∧” ⟩
    R ∩ R ⊆ R ∧ R ∩ R ⊆ R — This is “Weakening for ∩”

Theorem “Monotonicity of ∩”: Q ⊆ R  ⇒  Q ∩ S ⊆ R ∩ S
Proof:
    Q ⊆ R ⇒ Q ∩ S ⊆ R ∩ S
  ≡⟨ “Characterisation of ∩” ⟩
    Q ⊆ R ⇒ (Q ∩ S ⊆ R) ∧ (S ∩ Q ⊆ S)
  ≡⟨ “Idempotency of ∧” and “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:
  Using “Mutual implication”:
    Subproof for `Q ⊆ R  ⇒  Q ∩ R = Q`:
      Assuming `Q ⊆ R`:
          Q ∩ R = Q
        =⟨ “Mutual inclusion” ⟩
          Q ∩ R ⊆ Q ∧ Q ⊆ Q ∩ R
        =⟨ “Characterisation of ∩” ⟩
          Q ∩ R ⊆ Q ∧ Q ⊆ Q ∧ Q ⊆ R
        =⟨ “Reflexivity of ⊆”, Assumption `Q ⊆ R`, “Identity of ∧” ⟩
          Q ∩ R ⊆ Q
        =⟨ “Idempotency of ∧”, “Weakening for ∩” ⟩
          true
    Subproof for `Q ∩ R = Q ⇒ Q ⊆ R`:
      Assuming `Q ∩ R = Q`:
          Q ⊆ R
        =⟨ Assumption `Q ∩ R = Q` ⟩
          Q ∩ R ⊆ R
        =⟨ “Idempotency of ∧”, “Weakening for ∩” ⟩
          true

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
  =⟨ “Characterisation of ∩” ⟩
    (R ∩ S) ⊆  R ∩ S
  =⟨ “Reflexivity of ⊆” ⟩
    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) ˘
  =⟨ “Self-inverse of ˘”, “Isotonicity of ˘” ⟩
    (R ˘ ∩ S ˘) ˘ ⊆ (R ∩ S)
  =⟨ “Characterisation of ∩” ⟩
    (R ˘ ∩ S ˘) ˘ ⊆ R ∧ (R ˘ ∩ S ˘) ˘ ⊆ S
  =⟨ “Self-inverse of ˘”, “Isotonicity of ˘” ⟩
    R ˘ ∩ S ˘ ⊆ R ˘ ∧ R ˘ ∩ S ˘ ⊆ S ˘
  =⟨ “Weakening for ∩”, “Idempotency 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
  =⟨ “Definition of antisymmetry” ⟩
    R ∩ R ˘ ⊆ Id
  =⟨ “Self-inverse of ˘” ⟩
    R ˘ ∩ R ˘ ˘ ⊆ Id
  =⟨ “Definition of antisymmetry” ⟩
    is-antisymmetric (R ˘)

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