we added the standard notation for True and False (logical constants)

[helm.git] / matita / matita / lib / formal_topology / relations_to_o-algebra.ma

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 bc5153d5db66532004203625260f99767955eea9..48ac80da02696d4f93a7377fbf768e3854054959 100644 (file)
--- a/matita/matita/lib/formal_topology/relations_to_o-algebra.ma
+++ b/matita/matita/lib/formal_topology/relations_to_o-algebra.ma
@@ -22,9 +22,9 @@ definition POW': objs1 SET → OAlgebra.
   | apply overlaps;
   | apply big_intersects;
   | apply big_union;
-  | apply ({x | True});
+  | apply ({x | ⊤});
     simplify; intros; apply (refl1 ? (eq1 CPROP));
-  | apply ({x | False});
+  | apply ({x | ⊥});
     simplify; intros; apply (refl1 ? (eq1 CPROP));
   | intros; whd; intros; assumption
   | intros; whd; split; assumption