proposition: Corollary first_countable_sequence_closed {X : TopologicalSpace} (S : Ensemble X) : first_countable X -> (forall (x : Net nat_DS X) (x0 : X), (forall n : nat, In S (x n)) -> net_limit x x0 -> In S x0) -> closed S.
proof: Proof. intros. replace S with (closure S). { apply closure_closed. } apply Extensionality_Ensembles; split; red. 2: apply closure_inflationary. intros x Hx. apply first_countable_sequence_closure in Hx; auto. clear H. destruct Hx as [x0 [Hx0 Hx1]]. eapply H0; eauto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)