theorem Th15: :: DUALSP06:15

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