theorem Th22: :: MAZURULM:22

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