Theorem “Indirect ≤ from above”:
    x ≤ y  ≡   (∀ z : ℤ • y ≤ z ⇒ x ≤ z)
Proof:
  Using “Mutual implication”:
    Subproof for `x ≤ y ⇒ (∀ z : ℤ • y ≤ z ⇒ x ≤ z)`:
      Assuming `x ≤ y`:
        For any `z`:
            y ≤ z ⇒ x ≤ z
          ⇐⟨ “Transitivity of ≤” ⟩
            x ≤ y
          =⟨ Assumption `x ≤ y`⟩
            true
    Subproof for `(∀ z : ℤ • y ≤ z ⇒ x ≤ z) ⇒ x ≤ y`:
        (∀ z : ℤ • y ≤ z ⇒ x ≤ z)
      ⇒⟨ “Instantiation”⟩
        (y ≤ z ⇒ x ≤ z)[ z ≔ y ]
      =⟨ Substitution ⟩
        (y ≤ y ⇒ x ≤ y)
      =⟨ “Reflexivity of ≤”, “Left-identity of ⇒”⟩
        x ≤ y