proposition: Lemma ordering_function_seg_unicity : forall A1 A2 B, ordering_segment A1 B -> ordering_segment A2 B -> A1 = A2.
proof: Proof. destruct 1 as [f1 Hf1]; destruct 1 as [f2 Hf2]; apply Extensionality_Ensembles. assert (H : fun_equiv f1 f2 A1 A2) by (eapply ordering_function_unicity;eauto); now destruct H. Qed.
imports: ZornsLemma(CountableTypes)