theorem Th20: :: MAZURULM:20

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