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

x in Y

( 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

for x being object st x in W holds
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;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

x in Y

proof

hence
W = Y
by A8, TARSKI:2; :: thesis: verum
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;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