proposition: Lemma closure_fixes_closed : closed S -> closure = S.
proof: Proof. intro. apply Extensionality_Ensembles. split. - red. intros. destruct H0. apply H0; split; auto with sets. - apply closure_inflationary. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)