X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fformal_topology.ma;h=34a521f35f3d05e2a85295b51706596b0803e91c;hb=befe31089d1d45360b5b7681556c8a762800b3a2;hp=89ab9484ca5bcc51c69592273c92ba7b2e82923a;hpb=99ca90bf28a25fcd1cd84596c37be43c97f74e6e;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/formal_topology.ma b/helm/software/matita/contribs/formal_topology/formal_topology.ma
index 89ab9484c..34a521f35 100644
--- a/helm/software/matita/contribs/formal_topology/formal_topology.ma
+++ b/helm/software/matita/contribs/formal_topology/formal_topology.ma
@@ -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.
@@ -111,4 +110,4 @@ theorem th7: ∀A. i (m (i A)) = i (c (i (m (i A)))). intros; auto. qed.
 theorem th8: ∀A. i (m (i A)) = i (m (i (c (i A)))). intros; auto. qed.
 theorem th9: ∀A. i (c (m (c (i A)))) = i (m (i A)). intros; auto depth=4. qed.
 
-(* theorem th7: ∀A. i (m (i A)) = i (s (i A)). *)
\ No newline at end of file
+(* theorem th7: ∀A. i (m (i A)) = i (s (i A)). *)