proposition: Theorem position_relative_plans_general : 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) \/ confondus (plan A B C) (plan D E F)) \/ secants (plan A B C) (plan D E F).
proof: Proof. intros. assert (A <> B); auto with geo. assert (D <> E); auto with geo. elim (classic (para_plan_plan (plan A B C) (plan D E F))); intros. left; try assumption. apply position_relative_plans_paralleles; auto. right; try assumption. elim position_relative_plans with (A := A) (B := B) (C := C) (D := D) (E := E) (F := F); [ intros H4; try clear position_relative_plans | intros H4; try clear position_relative_plans; auto | auto | auto ]. tauto. Qed.