X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fsubsets.ma;h=254f924ddc7704bed995c16d36196ebe24e8abe1;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=108e3c7679eb19dd85700ca072c2599c4015a6ef;hpb=1ed4fe0f28d3b0b915387330cd722bfb80fb1063;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/subsets.ma b/helm/software/matita/library/formal_topology/subsets.ma
index 108e3c767..254f924dd 100644
--- a/helm/software/matita/library/formal_topology/subsets.ma
+++ b/helm/software/matita/library/formal_topology/subsets.ma
@@ -131,7 +131,7 @@ definition singleton: ∀A:setoid. A ⇒_1 Ω^A.
     intros; simplify;
     split; intro;
     apply (.= e1);
-     [ apply e | apply (e \sup -1) ]
+     [ apply e | apply (e^-1) ]
   | unfold setoid1_of_setoid; simplify;
     intros; split; intros 2; simplify in f ⊢ %; apply trans;
      [ apply a |4: apply a'] try assumption; apply sym; assumption]