let W, Y be set ; :: thesis: ( ( for x being set holds
( x in W iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ) & ( for x being set holds
( x in Y iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ) implies W = Y )

assume that
A2: for x being set holds
( x in W iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) and
A3: for x being set holds
( x in Y iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ; :: thesis: W = Y
A4: for x being object st x in Y holds
x in W
proof
let x be object ; :: thesis: ( x in Y implies x in W )
reconsider xx = x as set by TARSKI:1;
assume x in Y ; :: thesis: x in W
then ( xx c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) by A3;
hence x in W by A2; :: thesis: verum
end;
for x being object st x in W holds
x in Y
proof
let x be object ; :: thesis: ( x in W implies x in Y )
reconsider xx = x as set by TARSKI:1;
assume x in W ; :: thesis: x in Y
then ( xx c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) by A2;
hence x in Y by A3; :: thesis: verum
end;
hence W = Y by ; :: thesis: verum