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