theorem
for
S being
satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct for
a1,
a2 being
POINT of
S st
a1 <> a2 holds
ex
a3,
a4,
a5 being
POINT of
S st
(
between5 a1,
a2,
a3,
a4,
a5 &
a1,
a2,
a3,
a4,
a5 are_mutually_distinct )