....

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-basic_topologies.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index f2ce654bae925b1dd036d565c5aecf0a27351112..245fc4fdbf866ee9c9a28d521bb790c5f5cf4489 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -106,13 +106,13 @@ definition Ocontinuous_relation_comp:
   | intros;
     apply sym1; 
     change in match ((s ∘ r) U) with (s (r U));
-    apply (.= (Oreduced : ?)\sup -1);
+    apply (.= (Oreduced : ?)^-1);
      [ apply (.= (Oreduced :?)); [ assumption | apply refl1 ]
      | apply refl1]
   | intros;
     apply sym1;
     change in match ((s ∘ r)⎻* U) with (s⎻* (r⎻* U));
-    apply (.= (Osaturated : ?)\sup -1);
+    apply (.= (Osaturated : ?)^-1);
      [ apply (.= (Osaturated : ?)); [ assumption | apply refl1 ]
      | apply refl1]]
 qed.