theorem :: LOPBAN_1:28

for X, Y being RealNormSpace
for g being LinearOperator of X,Y holds
( g is Lipschitzian iff PreNorms g is bounded_above )