proposition: Lemma existence_pt_intersection : forall A B C D : PO, A <> B -> C <> D -> ~ alignes A B C \/ ~ alignes A B D -> concours (droite A B) (droite C D) -> exists I : PO, I = pt_intersection (droite A B) (droite C D) :>PO.
proof: Proof. intros. elim def_concours2 with (A := A) (B := B) (C := C) (D := D); [ intros I H3; elim H3; intros H4 H5; try clear H3 def_concours2; try exact H5 | auto | auto | auto ]. exists I. apply def_pt_intersection; auto. Qed.