theorem Th19: :: MAZURULM:19

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