proposition: Lemma cl_increasing: forall S1 S2:Ensemble X, Included S1 S2 -> Included (cl S1) (cl S2).
proof: Proof. intros. replace S2 with (Union S1 S2). - rewrite cl_respects_union. auto with sets. - extensionality_ensembles; auto with sets. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)