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

proof

let x be set ; :: 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;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in 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