Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
    is-reflexive Id
  ≡⟨ “Definition of reflexivity” ⟩
    ∀ x • x ⦗ Id ⦘ x
  ≡⟨ Subproof:
        For any `x`:
            x ⦗ Id ⦘ x
          ≡⟨ “Relationship via `Id`” ⟩
            x = x  — This is 【 “Reflexivity of =” 】
    ⟩
    true





Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
  Using “Definition of reflexivity”:
    Subproof for `∀ x • x ⦗ Id ⦘ x`:
      For any `x`:
          x ⦗ Id ⦘ x
        ≡⟨ “Relationship via `Id`” ⟩
          x = x  — This is “Reflexivity of =”





Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
  Using “Definition of reflexivity”:
    Subproof:
      For any `x`:
          x ⦗ Id ⦘ x
        ≡⟨ “Relationship via `Id`” ⟩
          x = x  — This is “Reflexivity of =”





Theorem “`Id` is reflexive”: is-reflexive Id
Proof:
  Using “Definition of reflexivity”:
    For any `x`:
        x ⦗ Id ⦘ x
      ≡⟨ “Relationship via `Id`” ⟩
        x = x  — This is “Reflexivity of =”





Theorem “Reflexivity”:  is-reflexive R  ≡  Id ⊆ R
Proof:
    Id ⊆ R
  =⟨ “Relation inclusion” ⟩
    ∀ x • (∀ y • (x ⦗ Id ⦘ y ⇒ x ⦗ R ⦘ y))
  =⟨ “Relationship via `Id`” ⟩
    ∀ x • (∀ y • (x = y ⇒ x ⦗ R ⦘ y))
  =⟨ “Trading for ∀” ⟩
    ∀ x • (∀ y ❙ x = y • x ⦗ R ⦘ y)
  =⟨ “One-point rule for ∀” ⟩
    ∀ x • ( (x ⦗ R ⦘ y)[y ≔ x])
  =⟨ Substitution ⟩
    ∀ x • ( (x ⦗ R ⦘ x))
  =⟨ “Definition of reflexivity” ⟩
    is-reflexive R





Theorem “Composition of reflexive relations”:
  is-reflexive R ⇒ is-reflexive S ⇒ is-reflexive (R ⨾ S)
Proof:
  Assuming `is-reflexive R`:
    Assuming `is-reflexive S`:
      Using “Definition of reflexivity”:
        For any `x`:
            x ⦗ R ⨾ S ⦘ x
          =⟨ “Relation composition” ⟩
            ∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x
          ⇐⟨ “∃-Introduction” ⟩
            (x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x)[b ≔ x]
          =⟨ Substitution ⟩
            x ⦗ R ⦘ x ∧ x ⦗ S ⦘ x
          =⟨ “Definition of reflexivity” with Assumption `is-reflexive R` ⟩
            true ∧ x ⦗ S ⦘ x
          =⟨ “Definition of reflexivity” with Assumption `is-reflexive S` ⟩
            true ∧ true
          =⟨ “Idempotency of ∧” ⟩
            true




Theorem “Composition of reflexive relations”:
  is-reflexive R ⇒ is-reflexive S ⇒ is-reflexive (R ⨾ S)
Proof:
  Assuming `is-reflexive R` and using with “Definition of reflexivity”:
    Assuming `is-reflexive S` and using with “Definition of reflexivity”:
      Using “Definition of reflexivity”:
        For any `x`:
            x ⦗ R ⨾ S ⦘ x
          =⟨ “Relation composition” ⟩
            ∃ b • x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x
          ⇐⟨ “∃-Introduction” ⟩
            (x ⦗ R ⦘ b ∧ b ⦗ S ⦘ x)[b ≔ x]
          =⟨ Substitution ⟩
            x ⦗ R ⦘ x ∧ x ⦗ S ⦘ x
          =⟨ Assumption `is-reflexive R` ⟩
            true ∧ x ⦗ S ⦘ x
          =⟨ Assumption `is-reflexive S` ⟩
            true ∧ true
          =⟨ “Idempotency of ∧” ⟩
            true




Theorem “Converse of reflexive relations”:
  is-reflexive R ⇒ is-reflexive (R ˘)
Proof:
  Assuming `is-reflexive R` and using with “Definition of reflexivity”:
    Using “Definition of reflexivity”:
      For any `x`:
          x ⦗ R ˘ ⦘ x
        =⟨ “Relation converse” ⟩
          x ⦗ R ⦘ x
        =⟨ Assumption `is-reflexive R` ⟩
          true





Theorem “Converse reflects reflectivity”:
  is-reflexive (R ˘) ⇒ is-reflexive R
Proof:
  Assuming `is-reflexive (R ˘)` and using with “Definition of reflexivity”:
    Using “Definition of reflexivity”:
      For any `x`:
          x ⦗ R ⦘ x
        =⟨ “Self-inverse of ˘”, “Relation converse” ⟩
          x ⦗ R ˘ ⦘ x
        =⟨ Assumption `is-reflexive (R ˘)` ⟩
          true





Theorem “Converse of transitive relations”:
    is-transitive R ⇒ is-transitive (R ˘)
Proof:
    Assuming `is-transitive R` and using with “Definition of transitivity”:
      Using “Definition of transitivity”:
        For any `x`, `y`, `z`:
            x ⦗ R ˘ ⦘ y ⦗ R ˘ ⦘ z  ⇒  x ⦗ R ˘ ⦘ z
          =⟨ “Reflexivity of =” ⟩
            x ⦗ R ˘ ⦘ y ∧ y ⦗ R ˘ ⦘ z  ⇒  x ⦗ R ˘ ⦘ z
          =⟨ “Relation converse” ⟩
            z ⦗ R ⦘ y ⦗ R ⦘ x ⇒  z ⦗ R ⦘ x
          =⟨ Assumption `is-transitive R` ⟩
            true