proposition: Lemma open_setminus {X : TopologicalSpace} (U V : Ensemble X) : open U -> closed V -> open (Setminus U V).
proof: Proof. intros. rewrite Setminus_Intersection. apply open_intersection2; assumption. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)