-theorem saturation_monotone:
- ∀C,A. is_saturation C A →
- ∀U,V. U ≤ V → A U ≤ A V.
- intros; apply (if ?? (H ??)); apply (oa_leq_trans C);
- [apply V|3: apply saturation_expansive ]
+theorem o_saturation_monotone: ∀C:OA.∀A:C ⇒_1 C. is_o_saturation C A → ∀U,V. U ≤ V → A U ≤ A V.
+ intros; apply (if ?? (i ??)); apply (oa_leq_trans C);
+ [apply V|3: apply o_saturation_expansive ]