proposition: Lemma closure_increasing: forall S T:Ensemble X, Included S T -> Included (closure S) (closure T).
proof: Proof. intros. apply closure_minimal. - apply closure_closed. - pose proof (closure_inflationary T). auto with sets. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)