fact: Definition Cr_fun : forall alpha : Ord, (forall beta : Ord, beta < alpha -> Ensemble Ord) -> Ensemble Ord := fun (alpha: Ord) (Cr : forall beta, beta < alpha -> Ensemble Ord) (x : Ord) => ( (alpha = zero /\ AP x) \/ (zero < alpha /\ forall beta (H:beta < alpha), In (the_ordering_segment (Cr beta H)) x /\ ord (Cr beta H) x = x)).
imports: Coq(Arith Logic.Epsilon Ensembles Classical) ZornsLemma(CountableTypes)