let A, B be Subset of ((FreeSort X) . s); :: thesis: ( ( for x being set holds

( x in A iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) ) & ( for x being set holds

( x in B iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) ) implies A = B )

assume that

A9: for x being set holds

( x in A iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) and

A10: for x being set holds

( x in B iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) ; :: 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 . s & x = root-tree [a,s] ) by A10;

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

( x in A iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) ) & ( for x being set holds

( x in B iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) ) implies A = B )

assume that

A9: for x being set holds

( x in A iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) and

A10: for x being set holds

( x in B iff ex a being set st

( a in X . s & x = root-tree [a,s] ) ) ; :: 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 . s & x = root-tree [a,s] ) by A9;

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

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

then ex a being set st

( a in X . s & x = root-tree [a,s] ) by A9;

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

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

then ex a being set st

( a in X . s & x = root-tree [a,s] ) by A10;

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