proposition: Lemma closure_minimal: forall F:Ensemble X, closed F -> Included S F -> Included closure F.
proof: Proof. intros. red. intros. destruct H1. apply H1. constructor; split; trivial. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)