for S being satisfying_Tarski-model TarskiGeometryStruct
for a, p, q, r, s being POINT of S holds
( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) )