big mess of notation

[helm.git] / helm / software / matita / library / formal_topology / subsets.ma

diff --git a/helm/software/matita/library/formal_topology/subsets.ma b/helm/software/matita/library/formal_topology/subsets.ma
index 108e3c7679eb19dd85700ca072c2599c4015a6ef..254f924ddc7704bed995c16d36196ebe24e8abe1 100644 (file)
--- 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]