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

[helm.git] / matita / matita / lib / formal_topology / basic_topologies_to_o-basic_topologies.ma

diff --git a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
index 58b75fb680ececa60755fcb2e77b7105b9245254..0aeb58c737a459c5b691a21561a37ba199cfa610 100644 (file)
--- a/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
+++ b/matita/matita/lib/formal_topology/basic_topologies_to_o-basic_topologies.ma
@@ -29,7 +29,7 @@ definition o_continuous_relation_of_continuous_relation:
   [ apply (orelation_of_relation ?? c) | apply (reduced ?? c) | apply (saturated ?? c) ]
 qed.
 
-axiom daemon: False.
+axiom daemon: ⊥. (*FG: alla faccia del costruttivismo *)
 
 lemma o_continuous_relation_of_continuous_relation_morphism :
   ∀S,T:category2_of_category1 BTop.