proposition: Lemma paralleles_orthogonal : forall A B C D E F : PO, A <> B -> C <> D -> paralleles (droite A B) (droite C D) -> orthogonal (vec A B) (vec E F) -> orthogonal (vec C D) (vec E F).
proof: Proof. intros. elim (paralleles_vecteur (A:=C) (B:=D) (C:=A) (D:=B)); auto with geo; intros. rewrite H3. Simplortho. Qed.