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