]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/formal_topology/bin/formal_topology.ma
some work
[helm.git] / helm / software / matita / contribs / formal_topology / bin / formal_topology.ma
index 1c1d94ad6d556715f2392f45ab761ae265e9b188..e84c0242ee8dd58a4225f9f8c10c27b2b924b73c 100644 (file)
@@ -22,8 +22,7 @@ axiom leq: S → S → Prop.
 notation "hvbox(A break ⊆ B)" with precedence 59
 for @{ 'subseteq $A $B}.
 
-interpretation "Subseteq" 'subseteq A B =
- (cic:/matita/formal_topology/leq.con A B).
+interpretation "Subseteq" 'subseteq A B = (leq A B).
 
 axiom leq_refl: ∀A. A ⊆ A.
 axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.