theorem :: GTARSKI3:110

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, p being POINT of S holds
( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b )