proposition: Theorem position_relative_plans : forall A B C D E F : PO, ~ alignes A B C -> ~ alignes D E F -> para_plan_plan (plan A B C) (plan D E F) \/ secants (plan A B C) (plan D E F).
proof: Proof. intros. lapply (plans_paralleles_ou_droite_incluse2 (A:=A) (B:=B) (C:=C) (D:=D) (E:=E) (F:=F)); intros; auto. elim H1; [ intros H2; try clear H1 | intros H2; elim H2; [ intros I H3; elim H3; [ intros J H4; elim H4; [ intros H5 H6; elim H6; [ intros H7 H8; try clear H6 H4 H3 H2 H1; try trivial ] ] ] ] | try trivial ]. left; try assumption. elim (classic (para_plan_plan (plan A B C) (plan D E F))); intros. left; try assumption. right; try assumption. apply def_secants with (I := I) (J := J); auto. Qed.