proposition: Lemma L3_u : exists! S, ordering_segment S B.
proof: Proof. exists (image B g); split. - apply image_B_g_seg. - intros ;eapply ordering_function_seg_unicity;eauto. apply image_B_g_seg. Qed.
imports: ZornsLemma(CountableTypes)