X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Frelations_to_o-algebra.ma;h=8030e28f665139f76dfa44a738ff8788c17eca0a;hb=d774b8f9c73e2497fb953e7feb4bc1840a464564;hp=48ac80da02696d4f93a7377fbf768e3854054959;hpb=bc477154d15f6979c948f9af602199af547d193e;p=helm.git

diff --git a/matita/matita/lib/formal_topology/relations_to_o-algebra.ma b/matita/matita/lib/formal_topology/relations_to_o-algebra.ma
index 48ac80da0..8030e28f6 100644
--- a/matita/matita/lib/formal_topology/relations_to_o-algebra.ma
+++ b/matita/matita/lib/formal_topology/relations_to_o-algebra.ma
@@ -14,7 +14,7 @@
 
 include "formal_topology/relations.ma".
 include "formal_topology/o-algebra.ma".
-
+(*
 definition POW': objs1 SET → OAlgebra.
  intro A; constructor 1;
   [ apply (Ω^A);
@@ -22,9 +22,9 @@ definition POW': objs1 SET → OAlgebra.
   | apply overlaps;
   | apply big_intersects;
   | apply big_union;
-  | apply ({x | ⊤});
+  | apply ({x | True});
     simplify; intros; apply (refl1 ? (eq1 CPROP));
-  | apply ({x | ⊥});
+  | apply ({x | False});
     simplify; intros; apply (refl1 ? (eq1 CPROP));
   | intros; whd; intros; assumption
   | intros; whd; split; assumption
@@ -238,4 +238,5 @@ change with (∀a1.(∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a) → a1 ∈ f a);
            [ intros 2; change in f3 with (eq1 ? a1 a2); change with (a2 ∈ f* a);
              apply (. f3^-1‡#); assumption;
            | assumption ]]]
-qed.
\ No newline at end of file
+qed.
+*)