theorem Th9: :: DUALSP06:9

for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V) holds x .|. (- y) = - (x .|. y)