proposition: Lemma paralleles_droite_incluse : forall A B C D E : PO, ~ alignes A B C -> D <> E -> incluse (droite D E) (plan A B C) -> para_plan_dr (plan A B C) (droite D E).
proof: Proof. intros. elim droite_incluse_plan with (A := A) (B := B) (C := C) (D := D) (E := E); intros; auto. apply def_para_plan_dr with (D := D) (E := E); auto with geo. Qed.