theorem A3: :: GTARSKI1:5

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st a,b equiv c,c holds
a = b