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 = exit (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 = exit (N,y) ) ) ) ) implies W = Y )
assume that
A6: 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 = exit (N,y) ) ) ) and
A7: 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 = exit (N,y) ) ) ) ; :: thesis: W = Y
A8: 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 = exit (N,y) ) ) by A7;
hence x in W by A6; :: 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 = exit (N,y) ) ) by A6;
hence x in Y by A7; :: thesis: verum

end;

hence W = Y by A8, TARSKI:1; :: thesis: verum