proposition: Lemma non_disjoints_exists : 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) -> exists I : PO, coplanaires A B C I /\ coplanaires D E F I.
proof: Proof. intros A B C D E F H H0 H1; try assumption. cut (~ (forall I : PO, ~ (coplanaires A B C I /\ coplanaires D E F I))); intros. elim not_all_not_ex with (U := PO) (P := fun I : PO => coplanaires A B C I /\ coplanaires D E F I); [ intros I H3; try clear not_all_not_ex; try exact H3 | auto ]. exists I; auto. red in |- *; (intros; apply H1). apply def_disjoints; auto. Qed.