X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fformal_topology%2Fbasic_pairs_to_basic_topologies.ma;h=fb8891613e75bbcf541e94e0fbd59b36dca5822a;hb=070b44c9c2344967ca8c4531909614a0d4da2fbe;hp=fe4cbd10f246e339c5191a9e3125000c0c039721;hpb=5fee26d2afb3a67370c92481bfbfdbd9ebed741e;p=helm.git

diff --git a/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
index fe4cbd10f..fb8891613 100644
--- a/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs_to_basic_topologies.ma
@@ -52,11 +52,13 @@ record functor1 (C1: category1) (C2: category1) : Type2 ≝
 
 (*
 definition BTop_of_BP: functor1 BP BTop.
- lapply OR as F;
  constructor 1;
   [ apply basic_topology_of_basic_pair
   | intros; constructor 1 [ apply continuous_relation_of_relation_pair; ]
   | simplify; intro;
   ]
 qed.
+
+lemma BBBB_faithful : failthful2 ?? VVV
+FIXME
 *)
\ No newline at end of file