proposition: Lemma droites_coplanaires : forall A B C D E F G : PO, D <> E -> F <> G -> ~ alignes A B C -> incluse (droite D E) (plan A B C) -> incluse (droite F G) (plan A B C) -> concours (droite D E) (droite F G) \/ paralleles (droite D E) (droite F G).
proof: Proof. intros A B C D E F G H10 H11 H H0 H1; try assumption. intros. elim (classic (paralleles (droite D E) (droite F G))); intros; auto. left; try assumption. elim droites_non_paralleles with (3 := H2); intros; auto. absurd (coplanaires F G D E); auto. elim droite_incluse_plan with (3 := H1); intros; auto. elim droite_incluse_plan with (3 := H0); intros; auto. apply coplanaire_trans3 with (A := A) (B := B) (C := C); auto. Qed.