proposition: Lemma paralleles_plan_droite_non_secants : forall A B C D E : PO, D <> E -> ~ alignes A B C -> para_plan_dr (plan A B C) (droite D E) -> ~ coplanaires A B C D -> ~ (exists I : PO, alignes D E I /\ coplanaires A B C I).
proof: Proof. intros. unfold not in |- *; intros. elim H3; intros I H4; elim H4; intros H5 H6; try clear H4 H3; try exact H6. elim def_para_plan_dr2 with (3 := H1); auto. intros F H3; elim H3; intros G H4; elim H4; intros H7 H8; elim H8; intros H9 H10; try clear H8 H4 H3; try exact H10. apply H2. cut (I <> D); intros. cut (para_plan_dr (plan A B C) (droite I D)); intros. apply paralleles_droite_plan_coplanaires_incluse with (3 := H4); auto. apply def_para_plan_dr with (D := F) (E := G); auto. elim H7; intros H13 H4; try clear H7; try exact H13. elim H7; intros H13 H4; try clear H7; try exact H4. apply paralleles_trans with D E; auto. generalize (alignes_paralleles (A:=D) (B:=E) (C:=I)); intros. apply paralleles_trans with D I; auto with geo. unfold not in |- *; intros; apply H2. rewrite <- H3; auto. Qed.