theorem A2: :: GTARSKI1:4

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds
p,q equiv r,s