set A = { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) 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 (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } c= TS (DTConMSA X)

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } is Subset of (TS (DTConMSA X)) ; :: thesis: verum

( x in X . s & a = root-tree [x,s] ) 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 (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } c= TS (DTConMSA X)

proof

hence
{ a where a is Element of TS (DTConMSA X) : ( ex x being set st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } or x in TS (DTConMSA X) )

assume x in { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } ; :: thesis: x in TS (DTConMSA X)

then ex a being Element of TS (DTConMSA X) st

( x = a & ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) ) ;

hence x in TS (DTConMSA X) ; :: thesis: verum

end;( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } or x in TS (DTConMSA X) )

assume x in { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } ; :: thesis: x in TS (DTConMSA X)

then ex a being Element of TS (DTConMSA X) st

( x = a & ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) ) ;

hence x in TS (DTConMSA X) ; :: thesis: verum

( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } is Subset of (TS (DTConMSA X)) ; :: thesis: verum