theorem Th4: :: MAZURULM:4

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