for S being TarskiGeometryStruct
for a, b, c being POINT of S st ( Middle a,b,c or between a,b,c ) holds
Collinear a,b,c