theorem Th17: :: MAZURULM:17

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