fact: Axiom def_para_plan_plan2 : 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) -> para_plan_dr (plan A B C) (droite D E) /\ para_plan_dr (plan A B C) (droite D F).