let A, B be Subset of (() . 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
proof
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;
let x be object ; :: 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 . s & x = root-tree [a,s] ) by A10;
hence x in A by A9; :: thesis: verum