theorem Satz7p9: :: GTARSKI3:103

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, p, p9 being POINT of S st reflection (a,p) = reflection (a,p9) holds
p = p9