X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fsaturations_to_o-saturations.ma;h=88a18fda7a38ecd5f8750f8b7d6e3bb1fe0a42b7;hb=8b1a49bbee9eea86eb74c040defe701370ca5893;hp=ce6c6f110ac571e7483bd9d51151eac80974783b;hpb=2857d1c432f073379552e1572235a86509b665a4;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
index ce6c6f110..88a18fda7 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
@@ -19,8 +19,8 @@ include "relations_to_o-algebra.ma".
 (* These are only conversions :-) *)
 
 definition o_operator_of_operator:
- ∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C).
- intros;apply t;
+ ∀C:REL. (Ω \sup C => Ω \sup C) → (POW C ⇒ POW C).
+ intros (C t);apply t;
 qed.
 
 definition is_o_saturation_of_is_saturation: