:: deftheorem DEFR defines reflection GTARSKI3:def 13 :
for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct
for a, p, b₄ being POINT of S holds
( b₄ = reflection (a,p) iff Middle p,a,b₄ );