Theorem “Relationship via 𝕀”: x ⦗ 𝕀 B ⦘ y  ≡  x = y ∈ B
Proof:
  Using “Mutual implication”:
    Subproof for `x ⦗ 𝕀 B ⦘ y  ⇒  x = y ∈ B`:
      Assuming `x ⦗ 𝕀 B ⦘ y`:
          x = y ∈ B
        =⟨ “Reflexivity of ≡” ⟩
          x = y ∧ y ∈ B
        =⟨ Substitution ⟩
          (z ∈ B)[z ≔ y] ∧ x = y
        =⟨ “Replacement” ⟩
          (z ∈ B)[z ≔ x] ∧ x = y
        =⟨ Substitution ⟩
          x ∈ B ∧ x = y
        =⟨ “Identity of ∧”, “Reflexivity of =” ⟩
          x ∈ B ∧ x = y ∧ x = x
        =⟨ Substitution ⟩
          (j ∈ B ∧ j = x ∧ j = y)[j ≔ x]
        ⇒⟨ “∃-Introduction” ⟩
          (∃ j • j ∈ B ∧ j = x ∧ j = y )
        =⟨ “Idempotency of ∧”, “Membership in ×”, “Trading for ∃” ⟩
          (∃ j ❙ ⟨ j , j ⟩ ∈ B × B • j = x ∧ j = y )
        =⟨ “Pair equality”, “Set membership”, “Reflexivity of =” ⟩
          ⟨ x , y ⟩ ∈ { x ❙ ⟨ x , x ⟩ ∈ B × B • ⟨ x , x ⟩ }
        =⟨ “Membership in ×”, “Idempotency of ∧”, “Definition of 𝕀”, “Definition of `_⦗_⦘_`” ⟩
          x ⦗ 𝕀 B ⦘ y
        =⟨ Assumption `x ⦗ 𝕀 B ⦘ y` with “Right-zero of ⇒” ⟩
          true


    Subproof for `x = y ∈ B ⇒ x ⦗ 𝕀 B ⦘ y`:
        x ⦗ 𝕀 B ⦘ y
      =⟨ “Definition of `_⦗_⦘_`” ⟩
        ⟨ x , y ⟩ ∈ 𝕀 B
      =⟨ “Definition of 𝕀” ⟩
        ⟨ x , y ⟩ ∈ { x ❙ x ∈ B • ⟨ x , x ⟩ }
      =⟨ “Idempotency of ∧”, “Membership in ×” ⟩
        ⟨ x , y ⟩ ∈ { x ❙ ⟨ x , x ⟩ ∈ B × B • ⟨ x , x ⟩ }
      =⟨ “Reflexivity of ≡”  ⟩
        ⟨ x , y ⟩ ∈ { j ❙ ⟨ j , j ⟩ ∈ B × B • ⟨ j , j ⟩ }
      =⟨ “Set membership” ⟩
        (∃ j ❙ ⟨ j , j ⟩ ∈ B × B • ⟨ j , j ⟩ = ⟨ x , y ⟩ )
      =⟨ “Pair equality” ⟩
        (∃ j ❙ ⟨ j , j ⟩ ∈ B × B • j = x ∧ j = y )
      =⟨ “Trading for ∃”, “Membership in ×”, “Idempotency of ∧” ⟩
        (∃ j • j ∈ B ∧ j = x ∧ j = y )
      ⇐⟨ “∃-Introduction” ⟩
        (j ∈ B ∧ j = x ∧ j = y)[j ≔ x]
      =⟨ Substitution ⟩
        (x ∈ B ∧ x = x ∧ x = y)
      =⟨ “Reflexivity of =” ⟩
        (x ∈ B ∧ true ∧ x = y)
      =⟨ “Identity of ∧” ⟩
        (x ∈ B ∧ x = y)
      =⟨ Substitution ⟩
        (z ∈ B)[z ≔ x] ∧ x = y
      =⟨ “Replacement” ⟩
        (z ∈ B)[z ≔ y] ∧ x = y
      =⟨ Substitution ⟩
        x = y ∧ y ∈ B
      =⟨ “Reflexivity of =” ⟩
        x = y ∈ B