proposition: Lemma position_relative_plan_droite_paralleles : forall A B C D E : PO, D <> E -> ~ alignes A B C -> para_plan_dr (plan A B C) (droite D E) -> incluse (droite D E) (plan A B C) \/ ~ contact (droite D E) (plan A B C).
proof: Proof. intros. elim (classic (coplanaires A B C D)); intros. left; try assumption. apply droite_incluse_plan2; auto. apply paralleles_droite_plan_coplanaires_incluse with D; auto. right; try assumption. generalize (paralleles_plan_droite_non_secants (A:=A) (B:=B) (C:=C) (D:=D) (E:=E)); intros H7. unfold not in |- *; intros. elim H7; try assumption. apply def_contact2; auto. Qed.