theorem :: GTARSKI3:100

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