proposition: Lemma closure_complement: forall S:Ensemble X, closure (Complement S) = Complement (interior S).
proof: Proof. intros. pose proof (interior_complement (Complement S)). rewrite Complement_Complement in H. now rewrite H, Complement_Complement. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)