set A = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } ;
{ a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } c= TS (DTConOSA X)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } or x in TS (DTConOSA X) )
assume x in { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } ; :: thesis: x in TS (DTConOSA X)
then ex a being Element of TS (DTConOSA X) st
( x = a & ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) ) ;
hence x in TS (DTConOSA X) ; :: thesis: verum

end;

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