defpred S_{1}[ object ] means $1 is Lipschitzian BilinearOperator of X,Y,Z;

consider IT being set such that

A1: for x being object holds

( x in IT iff ( x in BilinearOperators (X,Y,Z) & S_{1}[x] ) )
from XBOOLE_0:sch 1();

take IT ; :: thesis: ( IT is Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & ( for x being set holds

( x in IT iff x is Lipschitzian BilinearOperator of X,Y,Z ) ) )

for x being object st x in IT holds

x in BilinearOperators (X,Y,Z) by A1;

hence IT is Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by TARSKI:def 3; :: thesis: for x being set holds

( x in IT iff x is Lipschitzian BilinearOperator of X,Y,Z )

let x be set ; :: thesis: ( x in IT iff x is Lipschitzian BilinearOperator of X,Y,Z )

thus ( x in IT implies x is Lipschitzian BilinearOperator of X,Y,Z ) by A1; :: thesis: ( x is Lipschitzian BilinearOperator of X,Y,Z implies x in IT )

assume x is Lipschitzian BilinearOperator of X,Y,Z ; :: thesis: x in IT

hence x in IT by A1, EQSET; :: thesis: verum

consider IT being set such that

A1: for x being object holds

( x in IT iff ( x in BilinearOperators (X,Y,Z) & S

take IT ; :: thesis: ( IT is Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & ( for x being set holds

( x in IT iff x is Lipschitzian BilinearOperator of X,Y,Z ) ) )

for x being object st x in IT holds

x in BilinearOperators (X,Y,Z) by A1;

hence IT is Subset of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by TARSKI:def 3; :: thesis: for x being set holds

( x in IT iff x is Lipschitzian BilinearOperator of X,Y,Z )

let x be set ; :: thesis: ( x in IT iff x is Lipschitzian BilinearOperator of X,Y,Z )

thus ( x in IT implies x is Lipschitzian BilinearOperator of X,Y,Z ) by A1; :: thesis: ( x is Lipschitzian BilinearOperator of X,Y,Z implies x in IT )

assume x is Lipschitzian BilinearOperator of X,Y,Z ; :: thesis: x in IT

hence x in IT by A1, EQSET; :: thesis: verum