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

end;

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