theorem Prelim10:
for
S being non
empty satisfying_Tarski-model TarskiGeometryStruct for
a,
b,
c being
POINT of
S st (
Middle a,
b,
c or
Middle c,
b,
a ) & (
a <> b or
b <> c ) holds
(
Line (
b,
a)
= Line (
b,
c) &
Line (
a,
b)
= Line (
b,
c) &
Line (
a,
b)
= Line (
c,
b) &
Line (
b,
a)
= Line (
c,
b) )