defpred S₁[ object , object ] means ( $1 is Surreal & $2 is Surreal & $1 in X & $2 in Y & not $1 +' $2 == 0_No );
set S = { ((lamb +' (x1 *' y1)) * ((x1 +' y1) ")) where x1 is Element of X, y1 is Element of Y : S₁[x1,y1] } ;
{ ((lamb +' (x1 *' y1)) * ((x1 +' y1) ")) where x1 is Element of X, y1 is Element of Y : S₁[x1,y1] } is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in { ((lamb +' (x1 *' y1)) * ((x1 +' y1) ")) where x1 is Element of X, y1 is Element of Y : S₁[x1,y1] } or o is surreal )
assume o in { ((lamb +' (x1 *' y1)) * ((x1 +' y1) ")) where x1 is Element of X, y1 is Element of Y : S₁[x1,y1] } ; :: thesis: o is surreal
then ex x1 being Element of X ex y1 being Element of Y st
( o = (lamb +' (x1 *' y1)) * ((x1 +' y1) ") & S₁[x1,y1] ) ;
hence o is surreal ; :: thesis: verum

end;

then reconsider S = { ((lamb +' (x1 *' y1)) * ((x1 +' y1) ")) where x1 is Element of X, y1 is Element of Y : S₁[x1,y1] } as surreal-membered set ;
take S ; :: thesis: for o being object holds
( o in S iff ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) )
let o be object ; :: thesis: ( o in S iff ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) )
thus ( o in S implies ex x1, y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) ) :: thesis: ( ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) implies o in S )

proof

assume o in S ; :: thesis: ex x1, y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") )
then consider x1 being Element of X, y1 being Element of Y such that
A1: ( o = (lamb +' (x1 *' y1)) * ((x1 +' y1) ") & S₁[x1,y1] ) ;
reconsider x1 = x1, y1 = y1 as Surreal by A1;
take x1 ; :: thesis: ex y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") )
take y1 ; :: thesis: ( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") )
thus ( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) by A1; :: thesis: verum

end;

thus ( ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) implies o in S ) ; :: thesis: verum