proposition: Lemma closure_full : closure (@Full_set X) = Full_set.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. { constructor. } apply closure_inflationary. assumption. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)