theorem Satz7p13: :: GTARSKI3:105

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