proposition: Lemma closure_idempotent : idempotent (@closure X).
proof: Proof. intro. apply Extensionality_Ensembles. split. - red. intros. destruct H. apply H. constructor. split. + apply closure_closed. + red. now intros. - apply closure_inflationary. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)