proposition: Lemma compact_impl_net_cluster_point: forall X:TopologicalSpace, compact X -> forall (I:DirectedSet) (x:Net I X), inhabited (DS_set I) -> exists x0:X, net_cluster_point x x0.
proof: Proof. intros. destruct (compact_impl_filter_cluster_point _ H (tail_filter x H0)) as [x0]. exists x0. apply tail_filter_cluster_point_impl_net_cluster_point with H0. apply H1. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)