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 ; :: thesis: verum