theorem Th27: :: LOPBAN_1:27

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