set RT = { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } ;
{ [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } c= [:(TS (DTConOSA X)), the carrier of S:]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } or y in [:(TS (DTConOSA X)), the carrier of S:] )
assume y in { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } ; :: thesis: y in [:(TS (DTConOSA X)), the carrier of S:]
then consider s1 being Element of S such that
A1: y = [(root-tree t),s1] and
A2: ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) ;
consider s being Element of S, x being set such that
A3: x in X . s and
A4: t = [x,s] and
s <= s1 by A2;
root-tree [x,s] is Element of TS (DTConOSA X) by A3, Th10;
hence y in [:(TS (DTConOSA X)), the carrier of S:] by A1, A4, ZFMISC_1:def 2; :: thesis: verum

end;

hence { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } is Subset of [:(TS (DTConOSA X)), the carrier of S:] ; :: thesis: verum