proposition: Theorem ordering_function_ex : exists ! S, exists f, ordering_function f S B.
proof: Proof. Proof with eauto. case ordering_segment_ex_unique;intros S (f,pi); exists S. split. - case f;intros x H; exists x;auto. - intros x' H; case H; intros;case f;intros. eapply ordering_function_seg_unicity... Qed.
imports: ZornsLemma(CountableTypes)