fact: Definition one_aleph_of E := let r := worders_order E in let Z := Zo (worders_quo E) (fun z => ~ (segment r z) <s E) in let X0 := the_least (induced_order r Z) in let X1 := Yo (nonempty Z) (segment r X0) (worders_quo E) in (induced_order r X1).
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)