proposition: Lemma pt_intersection_commute : forall A B C D I : PO, A <> B :>PO -> C <> D :>PO -> ~ alignes A B C \/ ~ alignes A B D -> I = pt_intersection (droite A B) (droite C D) :>PO -> I = pt_intersection (droite C D) (droite A B) :>PO.
proof: Proof. intros. elim def_pt_intersection2 with (A := A) (B := B) (C := C) (D := D) (I := I); [ try clear def_pt_intersection2; intros | auto | auto | auto | auto ]. apply def_pt_intersection; auto. apply not_and_or; auto. cut (~ (alignes A B C /\ alignes A B D)); intros. red in |- *; intros; apply H5. apply ordre_alignement_4points; auto. apply or_not_and; auto. Qed.