fact: Definition open_cover {X : TopologicalSpace} (F : Family X) : Prop := (forall U, In F U -> open U) /\ (FamilyUnion F = Full_set).
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)