theorem Satz8p22lemma:
for
S being non
empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct for
a,
b,
p,
q,
t being
POINT of
S st
a,
p <= b,
q &
are_orthogonal a,
b,
q,
b &
are_orthogonal a,
b,
p,
a &
Collinear a,
b,
t &
between q,
t,
p holds
ex
x being
POINT of
S st
Middle a,
x,
b