theorem :: DUALSP01:22

for X being RealNormSpace
for g being linear-Functional of X holds
( g is Lipschitzian iff PreNorms g is bounded_above )