theorem Prelim10: :: GTARSKI4:10
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) )