proposition: Lemma paralleles_droites_plan_trans : forall A B C D E F G : PO, ~ alignes A B C -> D <> E :>PO -> F <> G :>PO -> para_plan_dr (plan A B C) (droite D E) -> paralleles (droite D E) (droite F G) -> para_plan_dr (plan A B C) (droite F G).
proof: Proof. intros. elim def_para_plan_dr2 with (A := A) (B := B) (C := C) (F := D) (G := E); [ intros D0 H5; elim H5; intros E0 H6; elim H6; intros H7 H8; elim H8; intros H9 H10; try clear H8 H6 H5 def_para_plan_dr2; try exact H10 | auto | auto | auto ]. apply def_para_plan_dr with (D := D0) (E := E0); auto. elim H6; intros H4 H11; elim H4; intros H12 H13; try clear H4 H6; try exact H12. elim H7; intros H4 H11; try clear H7; try exact H11. apply paralleles_trans with (4 := H10); auto. Qed.