theorem Th30: :: DUALSP01:24

for X being RealNormSpace
for f being Lipschitzian linear-Functional of X holds (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms f)