fact: Definition maximal_critical alpha : Ensemble Ord := fun gamma => In (Cr alpha) gamma /\ forall xi, alpha < xi -> ~ In (Cr xi) gamma.
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)