theorem Th23: :: MAZURULM:23

for E being RealNormSpace
for a being Point of E holds (a -reflection) /" = a -reflection