proposition: Lemma orthogonaux_orthogonales_toute_droite : forall A B C D E F G : PO, ~ alignes A B C -> D <> E -> F <> G -> coplanaires A B C F -> coplanaires A B C G -> orthogonaux (droite D E) (plan A B C) -> orthogonales (droite F G) (droite D E).
proof: Proof. intros. assert (A <> B); auto with geo. apply orthogonales_2droites_secantes with (1 := H); auto. elim def_orthogonaux2 with (A := A) (B := B) (C := C) (D := D) (E := E); [ try clear def_orthogonaux2; intros; auto | auto | auto | auto ]. elim def_orthogonaux2 with (A := A) (B := B) (C := C) (D := D) (E := E); [ try clear def_orthogonaux2; intros; auto | auto | auto | auto ]. Qed.