...

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma
index 6b6469f271e72380c0fb08bdfddd6322737ff051..ee9682cecd605dfc1047a2b459e2a3425b6f7883 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma
@@ -19,7 +19,7 @@ include "relations_to_o-algebra.ma".
 definition o_basic_topology_of_basic_topology: cic:/matita/formal_topology/basic_topologies/basic_topology.ind#xpointer(1/1) → basic_topology.
  intro;
  constructor 1;
-  [ apply (SUBSETS b);
+  [ apply (POW' b);
   | apply (A b);
   | apply (J b);
   | apply (A_is_saturation b);

diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
index 97bfcd6c9d19aac7ea9c591209479db41d5fbc13..88a18fda7a38ecd5f8750f8b7d6e3bb1fe0a42b7 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
@@ -19,7 +19,7 @@ include "relations_to_o-algebra.ma".
 (* These are only conversions :-) *)
 
 definition o_operator_of_operator:
- ∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C).
+ ∀C:REL. (Ω \sup C => Ω \sup C) → (POW C ⇒ POW C).
  intros (C t);apply t;
 qed.