-definition is_o_saturation_of_is_saturation: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
- is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
- intros; apply i;
-qed.
+definition is_o_saturation_of_is_saturation:
+ ∀C:REL.∀R: Ω^C ⇒_1 Ω^C. is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
+intros (C R i); apply i; qed.