let A, B be set ; :: thesis: ( ( for x being set holds

( x in A iff ex a being set st

( a in X . i & x = [a,i] ) ) ) & ( for x being set holds

( x in B iff ex a being set st

( a in X . i & x = [a,i] ) ) ) implies A = B )

assume that

A4: for x being set holds

( x in A iff ex a being set st

( a in X . i & x = [a,i] ) ) and

A5: for x being set holds

( x in B iff ex a being set st

( a in X . i & x = [a,i] ) ) ; :: thesis: A = B

thus A c= B :: according to XBOOLE_0:def 10 :: thesis: B c= A

assume x in B ; :: thesis: x in A

then ex a being set st

( a in X . i & x = [a,i] ) by A5;

hence x in A by A4; :: thesis: verum

( x in A iff ex a being set st

( a in X . i & x = [a,i] ) ) ) & ( for x being set holds

( x in B iff ex a being set st

( a in X . i & x = [a,i] ) ) ) implies A = B )

assume that

A4: for x being set holds

( x in A iff ex a being set st

( a in X . i & x = [a,i] ) ) and

A5: for x being set holds

( x in B iff ex a being set st

( a in X . i & x = [a,i] ) ) ; :: thesis: A = B

thus A c= B :: according to XBOOLE_0:def 10 :: thesis: B c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in A )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )

assume x in A ; :: thesis: x in B

then ex a being set st

( a in X . i & x = [a,i] ) by A4;

hence x in B by A5; :: thesis: verum

end;assume x in A ; :: thesis: x in B

then ex a being set st

( a in X . i & x = [a,i] ) by A4;

hence x in B by A5; :: thesis: verum

assume x in B ; :: thesis: x in A

then ex a being set st

( a in X . i & x = [a,i] ) by A5;

hence x in A by A4; :: thesis: verum