Theorem “Isotonicity of 𝕀”:  B ⊆ C  ≡  𝕀 B ⊆ 𝕀 C
Proof:
    𝕀 B ⊆ 𝕀 C
  =⟨ “Relation inclusion” ⟩
    (∀ x • ∀ y • x ⦗ 𝕀 B ⦘ y ⇒ x ⦗ 𝕀 C ⦘ y)
  =⟨ “Relationship via 𝕀” ⟩
    (∀ x • ∀ y • x = y ∧ y ∈ B ⇒ x = y ∧ y ∈ C)
  =⟨ “Shunting” ⟩
    (∀ x • ∀ y • x = y ⇒ y ∈ B ⇒ x = y ∧ y ∈ C)
  =⟨ Substitution ⟩
    (∀ x • ∀ y • x = y ⇒ (y ∈ B ⇒ w = y ∧ y ∈ C)[w ≔ x])
  =⟨ “Replacement”, Substitution ⟩
    (∀ x • ∀ y • x = y ⇒ (y ∈ B ⇒ y = y ∧ y ∈ C))
  =⟨ “Reflexivity of =”, “Identity of ∧” ⟩
    (∀ x • ∀ y • x = y ⇒ y ∈ B ⇒ y ∈ C)
  =⟨ “Trading for ∀” ⟩
    (∀ x • ∀ y ❙ x = y • y ∈ B ⇒ y ∈ C)
  =⟨ “One-point rule for ∀” ⟩
    (∀ x • (y ∈ B ⇒ y ∈ C)[y ≔ x])
  =⟨ Substitution ⟩
    (∀ x • x ∈ B ⇒ x ∈ C)
  =⟨ “Set inclusion” ⟩
    B ⊆ C