notation "hvbox(A break ⊆ B)" with precedence 59
for @{ 'subseteq $A $B}.
-interpretation "Subseteq" 'subseteq A B = (eq _ A (comp eps B)).
+interpretation "Subseteq" 'subseteq A B = (eq ? A (comp eps B)).
axiom leq_refl: ∀A. A ⊆ A.
axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.