proposition: Theorem position_relative_plans_non_disjoints : forall A B C D E F : PO, ~ alignes A B C -> ~ alignes D E F -> ~ disjoints (plan A B C) (plan D E F) -> secants (plan A B C) (plan D E F) \/ confondus (plan A B C) (plan D E F).
proof: Proof. intros. elim position_relative_plans_general with (A := A) (B := B) (C := C) (D := D) (E := E) (F := F); [ intros H2; elim H2; [ intros H3; try clear H2 position_relative_plans_general | intros H3; try clear H2 position_relative_plans_general; try exact H3 ] | intros H2 | auto | auto ]. elim H2; [ intros H4; try clear H2 | intros H4; try clear H2; try exact H4 ]. tauto. right; try assumption. elim H2; [ intros H4; try clear H2; try exact H4 | intros H4; try clear H2 ]. tauto. right; try assumption. left; try assumption. Qed.