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`:
          (∀ z : ℤ • y ≤ z ⇒ x ≤ z)
        ≡⟨ “Transitivity of ≤” with Assumption `x ≤ y` ⟩
          (∀ z : ℤ • true)
        ≡⟨ “True ∀ body” ⟩
          true
    Subproof for `(∀ z : ℤ • y ≤ z ⇒ x ≤ z) ⇒ x ≤ y`:
      Assuming `(∀ z : ℤ • y ≤ z ⇒ x ≤ z)`:
          x ≤ y
        ⇒⟨ “Transitivity of ≤” ⟩
          y ≤ z ⇒ x ≤ z
        ≡⟨ ? ⟩
          true