Theorem “Indirect set equality from below”:
   S = T  ≡  (∀ Q • Q ⊆ S ≡ Q ⊆ T)
Proof:
  Using “Mutual implication”:
    Subproof for `S = T ⇒ (∀ Q • Q ⊆ S ≡ Q ⊆ T)`:
      Assuming `S = T`:
          (∀ Q • Q ⊆ S ≡ Q ⊆ T)
        ≡⟨ Assumption `S = T` ⟩
          (∀ Q • Q ⊆ S ≡ Q ⊆ S)
        ≡⟨ “Reflexivity of ≡” ⟩
          (∀ Q • true)
        ≡⟨ “True ∀ body” ⟩
          true
    Subproof for `(∀ Q • Q ⊆ S ≡ Q ⊆ T) ⇒ S = T`:
      Assuming `(∀ Q • Q ⊆ S ≡ Q ⊆ T)`:
          S = T
        ≡⟨ ? ⟩
          true