fact: Definition Closed (B : Ensemble Ord) : Prop := forall M, Included M B -> Inhabited M -> Countable M -> In B (|_| M).
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)