theorem :: GTARSKI3:109

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