...

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

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);