theorem Th2: :: DUALSP06:2

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