for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for x, y, z, a, b, c, c9, p, q, q9 being POINT of S st not Collinear a,b,c & between b,a,y & a <> y & between a,y,z & y,z equiv y,p & y <> p & q9 = reflection (z,q) & Middle c,x,c9 & c <> y & between q9,y,c9 & Middle y,p,c & between p,y,q & q <> q9 holds
x <> y