for E being RealNormSpace
for a being Point of E holds (a -reflection) * (a -reflection) = id E