theorem C1prime: :: GTARSKI1:26

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, x, y being POINT of S st a <> b & between a,b,x & between a,b,y & a,x equiv a,y holds
x = y