(* 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: