Positive Lω1ω definitions of point-inequality and noncollinearity in terms of collinearity, which are valid in plane hyperbolic geometry
over arbitrary Archimedean ordered Euclidean fields, provide a synthetic proof of the theorem stated in the title and first
noticed to be a corollary of a result from  by R. Höfer .
We present an axiom system for plane hyperbolic geometry in a language with lines as the only individual variables and the
binary relation of line-perpendicularity as the only primitive notion. It was made possible by results obtained by K. List
and H.L. Skala. A similar axiomatization is possible for n-dimensional hyperbolic geometry with n≥4. We also point out that plane hyperbolic geometry admits a AE-axiomatization in terms of line-perpendicularity alone, an
axiomatization we could not find.