:: deftheorem Def9 defines BoundedBilinearOperators LOPBAN_9:def 4 :
for X, Y, Z being RealNormSpace
for b₄ being Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds
( b₄ = BoundedBilinearOperators (X,Y,Z) iff for x being set holds
( x in b₄ iff x is Lipschitzian BilinearOperator of X,Y,Z ) );