X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Frelations.ma;fp=matita%2Fmatita%2Flib%2Fformal_topology%2Frelations.ma;h=2d5d85a6be9a1dc0cca55b46d702694b655712a8;hb=716338697e54d7a7e3602aabdecc2a8a639d683e;hp=2ad35655e51756a1ceceda01182f1c126b0100f2;hpb=e31d9eb44ea0e5dd472e10282a826bdba2126810;p=helm.git

diff --git a/matita/matita/lib/formal_topology/relations.ma b/matita/matita/lib/formal_topology/relations.ma
index 2ad35655e..2d5d85a6b 100644
--- a/matita/matita/lib/formal_topology/relations.ma
+++ b/matita/matita/lib/formal_topology/relations.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "formal_topology/subsets.ma".
-
+(*
 record binary_relation (A,B: SET) : Type[1] ≝
  { satisfy:> binary_morphism1 A B CPROP }.
 
@@ -323,4 +323,5 @@ theorem extS_singleton:
  intros; unfold extS; unfold ext; unfold singleton; simplify;
  split; intros 2; simplify; simplify in f; 
  [ cases f; cases e; cases x1; change in f2 with (x =_1 w); apply (. #‡f2); assumption;
- | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
\ No newline at end of file
+ | split; try apply I; exists [apply x] split; try assumption; change with (x = x); apply rule #;] qed.
+*)