X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fsubsets.ma;h=56c2c895cbb98d2495b099e88c919792481075d2;hb=74223db3fc45caccb3cfac80971b29cb0613da28;hp=8bacd2a5538ce15df4168e0e9675a69d69dd69c0;hpb=eaaea3c18083de3e442e939768ff450d3b093911;p=helm.git

diff --git a/matita/matita/lib/formal_topology/subsets.ma b/matita/matita/lib/formal_topology/subsets.ma
index 8bacd2a55..56c2c895c 100644
--- a/matita/matita/lib/formal_topology/subsets.ma
+++ b/matita/matita/lib/formal_topology/subsets.ma
@@ -13,7 +13,9 @@
 (**************************************************************************)
 
 include "formal_topology/categories.ma".
-
+include "basics/core_notation/singl_1.ma".
+include "basics/core_notation/subset_1.ma".
+(*
 record powerset_carrier (A: objs1 SET) : Type[1] ≝ { mem_operator: A ⇒_1 CPROP }.
 interpretation "powerset low" 'powerset A = (powerset_carrier A).
 notation "hvbox(a break ∈. b)" non associative with precedence 45 for @{ 'mem_low $a $b }.
@@ -179,3 +181,4 @@ interpretation "bigcup" 'bigcup f = (fun12 ?? (big_union ??) f).
 interpretation "bigcap" 'bigcap f = (fun12 ?? (big_intersects ??) f).
 interpretation "bigcup mk" 'bigcup_mk f = (fun12 ?? (big_union ??) (mk_unary_morphism2 ?? f ?)).
 interpretation "bigcap mk" 'bigcap_mk f = (fun12 ?? (big_intersects ??) (mk_unary_morphism2 ?? f ?)).
+*)