proposition: Lemma finite_topology_compact (X : TopologicalSpace) : Finite (@open X) -> compact X.
proof: Proof. intros. red. intros. exists C. repeat split; auto with sets. apply Finite_downward_closed with (A := open); assumption. Qed.
imports: Coq(ClassicalChoice Program.Subset) ZornsLemma(Finite_sets Powerset_facts) Topology(FiltersAndNets)