set NT = { [((Den o2,(ParsedTermsOSA X)) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args o2,(ParsedTermsOSA X), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } ;
{ [((Den o2,(ParsedTermsOSA X)) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args o2,(ParsedTermsOSA X), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } c= [:(TS (DTConOSA X)),the carrier of S:]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { [((Den o2,(ParsedTermsOSA X)) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args o2,(ParsedTermsOSA X), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } or y in [:(TS (DTConOSA X)),the carrier of S:] )
assume y in { [((Den o2,(ParsedTermsOSA X)) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args o2,(ParsedTermsOSA X), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } ; :: thesis: y in [:(TS (DTConOSA X)),the carrier of S:]
then consider o2 being OperSymbol of S, x2 being Element of Args o2,(ParsedTermsOSA X), s3 being Element of S such that
A1: y = [((Den o2,(ParsedTermsOSA X)) . x2),s3] and
ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) and
ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ;
A2: OSSym o2,X ==> roots x2 by Th13;
A3: x2 is FinSequence of TS (DTConOSA X) by Th13;
then A4: (OSSym o2,X) -tree x2 in TS (DTConOSA X) by A2, Th12;
consider o being OperSymbol of S such that
A5: OSSym o2,X = [o,the carrier of S] and
x2 in Args o,(ParsedTermsOSA X) and
A6: (OSSym o2,X) -tree x2 = (Den o,(ParsedTermsOSA X)) . x2 and
for s1 being Element of S holds
( (OSSym o2,X) -tree x2 in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) by A3, A2, Th12;
o2 = o by A5, ZFMISC_1:33;
hence y in [:(TS (DTConOSA X)),the carrier of S:] by A1, A4, A6, ZFMISC_1:def 2; :: thesis: verum

end;

hence { [((Den o2,(ParsedTermsOSA X)) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args o2,(ParsedTermsOSA X), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) ) } is Subset of [:(TS (DTConOSA X)),the carrier of S:] ; :: thesis: verum