theorem C1: :: GTARSKI1:15

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 & b,x equiv b,y holds
x = y