A9.2

Theorem “Modal rule”:
    (Q ⨾ R) ∩ S ⊆ (Q ∩ S ⨾ R ˘) ⨾ R
Proof:
    (Q ⨾ R) ∩ S
  ⊆⟨ “Dedekind rule” ⟩
    (Q ∩ S ⨾ R ˘) ⨾ (R ∩ Q ˘ ⨾ S)
  ⊆⟨ Monotonicity with “Weakening for ∩” ⟩
    (Q ∩ S ⨾ R ˘) ⨾ R

Theorem “Modal rule”:
    (Q ⨾ R) ∩ S ⊆ Q ⨾ (R ∩ Q ˘ ⨾ S)
Proof:
    (Q ⨾ R) ∩ S
  ⊆⟨ “Dedekind rule” ⟩
    (Q ∩ S ⨾ R ˘) ⨾ (R ∩ Q ˘ ⨾ S)
  ⊆⟨ Monotonicity with “Weakening for ∩” ⟩
    Q ⨾ (R ∩ Q ˘ ⨾ S)

Theorem “Hesitation”: R ⊆ R ⨾ R ˘ ⨾ R
Proof:
    R
  =⟨ “Idempotency of ∩” ⟩
    R ∩ R
  =⟨ “Identity of ⨾” ⟩
    Id ⨾ R ∩ R
  ⊆⟨ “Modal rule” ⟩
    (Id ∩ R ⨾ R ˘) ⨾ R
  ⊆⟨ Monotonicity with “Weakening for ∩” ⟩
    R ⨾ R ˘ ⨾ R

Theorem “PER factoring”:
    is-symmetric Q ⇒ is-transitive Q ⇒  Q ⨾ R ∩ Q = Q ⨾ (R ∩ Q)
Proof:
  Assuming `is-symmetric Q` and using with “Definition of symmetry”,
           `is-transitive Q` and using with “Definition of transitivity”:
      Q ⨾ (R ∩ Q)
    ⊆⟨ “Sub-distributivity of ⨾ over ∩” ⟩
      Q ⨾ R ∩ Q ⨾ Q
    ⊆⟨ Monotonicity with assumption `is-transitive Q` ⟩
      Q ⨾ R ∩ Q
    ⊆⟨ “Modal rule” ⟩
      Q ⨾ (R ∩ Q ˘ ⨾ Q)
    ⊆⟨ Monotonicity with assumption `is-symmetric Q` ⟩
      Q ⨾ (R ∩ Q ⨾ Q)
    ⊆⟨ Monotonicity with assumption `is-transitive Q` ⟩
      Q ⨾ (R ∩ Q)

Theorem “Reflexive implies total”:
    is-reflexive R  ⇒  is-total R
Proof:
  Assuming `is-reflexive R` and using with “Definition of reflexivity”:
      Side proof for `Id ⊆ R ˘`:
          Id ⊆ R — This is assumption `is-reflexive R`
        ≡⟨ “Isotonicity of ˘” ⟩
          Id ˘ ⊆ R ˘
        ≡⟨ “Converse of `Id`” ⟩
          Id ⊆ R ˘
      Continuing:
          Id ⊆ R — This is assumption `is-reflexive R`
        ⇒⟨ “Monotonicity of ⨾” ⟩
          Id ⨾ R ˘ ⊆ R ⨾ R ˘
        ≡⟨ “Identity of ⨾” ⟩
          R ˘ ⊆ R ⨾ R ˘
        ⇒⟨ “Transitivity of ⊆” with local property `Id ⊆ R ˘` ⟩
          Id ⊆ R ⨾ R ˘
        ≡⟨ “Definition of totality” ⟩
          is-total R

Theorem “Swapping mapping across ⊆”:
    is-mapping F  ⇒  (R ⨾ F ⊆ S  ≡  R ⊆ S ⨾ F ˘)
Proof:
  Assuming `is-mapping F` and using with “Definition of mappings”:
      R ⊆ S ⨾ F ˘
    ⇒⟨ “Monotonicity of ⨾” ⟩
      R ⨾ F ⊆ S ⨾ F ˘ ⨾ F
    ⇒⟨ Monotonicity with assumption `is-mapping F` ⟩
      R ⨾ F ⊆ S ⨾ Id
    ≡⟨ “Identity of ⨾” ⟩
      R ⨾ F ⊆ S
    ⇒⟨ “Monotonicity of ⨾” ⟩
      R ⨾ F ⨾ F ˘ ⊆ S ⨾ F ˘
    ⇒⟨ “Transitivity of ⊆” with Monotonicity with assumption `is-mapping F` ⟩
      R ⨾ Id ⊆ S ⨾ F ˘
    ≡⟨ “Identity of ⨾” ⟩
      R ⊆ S ⨾ F ˘