X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fo-saturations.ma;h=8a9befa68f3c8d1a947faf14c04719e92bc4e32f;hb=3c257bf84769adf162510ed86a89872e3003629a;hp=20db479a314f9612cc00980dd791846136abf329;hpb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;p=helm.git

diff --git a/matita/matita/lib/formal_topology/o-saturations.ma b/matita/matita/lib/formal_topology/o-saturations.ma
index 20db479a3..8a9befa68 100644
--- a/matita/matita/lib/formal_topology/o-saturations.ma
+++ b/matita/matita/lib/formal_topology/o-saturations.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "formal_topology/o-algebra.ma".
-
+(*
 definition is_o_saturation: ∀C:OA. C ⇒_1 C → CProp[1] ≝
  λC:OA.λA:C ⇒_1 C.∀U,V. (U ≤ A V) =_1 (A U ≤ A V).
 
@@ -35,3 +35,4 @@ theorem o_saturation_idempotent: ∀C:OA.∀A:C ⇒_1 C. is_o_saturation C A →
   [ apply (if ?? (i (A U) U)); apply (oa_leq_refl C).
   | apply o_saturation_expansive; assumption]
 qed.
+*)