theorem Satz8p21:
for
S being non
empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct for
a,
b,
c being
POINT of
S st
a <> b holds
ex
p,
t being
POINT of
S st
(
are_orthogonal a,
b,
p,
a &
Collinear a,
b,
t &
between c,
t,
p )