proposition: Lemma th_In A alpha : In (the_ordering_segment A) alpha -> In A (ord A alpha).
proof: Proof. unfold ord; intro H; red; unfold some; apply epsilon_ind. - destruct (ordering_function_ex A) as [X [[f Hf] H0]]; exists f. rewrite <- (H0 (the_ordering_segment A) ); auto. exists (ord A); apply ord_ok. - intros beta H0; eapply ordering_function_In; [ eexact H0 | trivial]. Qed.
imports: ZornsLemma(CountableTypes)