proposition: Lemma interior_complement: forall S:Ensemble X, interior (Complement S) = Complement (closure S).
proof: Proof. intros. apply Extensionality_Ensembles; split. - rewrite <- Complement_Complement with (A:=interior (Complement S)). apply complement_inclusion. apply closure_minimal. + red. rewrite Complement_Complement. apply interior_open. + pattern S at 1. rewrite <- Complement_Complement with (A:=S). apply complement_inclusion. apply interior_deflationary. - apply interior_maximal. + apply closure_closed. + apply complement_inclusion. apply closure_inflationary. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)