:: deftheorem Def4 defines -reflection MAZURULM:def 4 :
for E being non empty RLSStruct
for a being Point of E
for b₃ being UnOp of E holds
( b₃ = a -reflection iff for b being Point of E holds b₃ . b = (2 * a) - b );