theorem A1: :: GTARSKI1:3

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