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 set st x in Y holds
x in W

proof

let x be set ; :: thesis: ( x in Y implies x in W )
assume x in Y ; :: thesis: x in W
then ( x 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 set st x in W holds
x in Y

proof

let x be set ; :: thesis: ( x in W implies x in Y )
assume x in W ; :: thesis: x in Y
then ( x 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 A4, TARSKI:1; :: thesis: verum