let C be set ; :: thesis: ( C = comp (X,x,y,Y) iff for o being object holds
( o in C iff ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) ) )
thus ( C = comp (X,x,y,Y) implies for o being object holds
( o in C iff ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) ) ) :: thesis: ( ( for o being object holds
( o in C iff ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) ) ) implies C = comp (X,x,y,Y) )

proof

assume A1: C = comp (X,x,y,Y) ; :: thesis: for o being object holds
( o in C iff ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) )
let o be object ; :: thesis: ( o in C iff ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) )
thus ( o in C implies ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) ) :: thesis: ( ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) implies o in C )

proof

assume o in C ; :: thesis: ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y )
then consider x1, y1 being Surreal such that
A2: ( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) by A1, Def14;
o = ((x1 * y) + (x * y1)) - (x1 * y1) by A2;
hence ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) by A2; :: thesis: verum

end;

assume ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) ; :: thesis: o in C
hence o in C by A1, Def14; :: thesis: verum

end;

assume A3: for o being object holds
( o in C iff ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) ) ; :: thesis: C = comp (X,x,y,Y)
thus C c= comp (X,x,y,Y) :: according to XBOOLE_0:def 10 :: thesis: comp (X,x,y,Y) c= C

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in C or o in comp (X,x,y,Y) )
assume A4: o in C ; :: thesis: o in comp (X,x,y,Y)
ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) by A4, A3;
hence o in comp (X,x,y,Y) by Def14; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in comp (X,x,y,Y) or o in C )
assume A5: o in comp (X,x,y,Y) ; :: thesis: o in C
consider x1, y1 being Surreal such that
A6: ( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) by A5, Def14;
o = ((x1 * y) + (x * y1)) - (x1 * y1) by A6;
hence o in C by A6, A3; :: thesis: verum