for E being RealNormSpace
for a being Point of E holds
( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds
a = b ) )