X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Fformal_topology2.ma;h=0896edc5ce9f572dbea7e55897e89e8d94ad462d;hb=bbf85ddcdfe0809fee0c6ca9812ce0da30c238af;hp=10666ba35d010c169827c24266cacc099e1444fa;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/formal_topology2.ma b/helm/software/matita/contribs/formal_topology/formal_topology2.ma
index 10666ba35..0896edc5c 100644
--- a/helm/software/matita/contribs/formal_topology/formal_topology2.ma
+++ b/helm/software/matita/contribs/formal_topology/formal_topology2.ma
@@ -38,7 +38,7 @@ axiom eps_idempotent: eps = eps eps.
 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.