set D = DTConOSA X;
defpred S₁[ set ] means ex s being SortSymbol of S st
( $1 in the Sorts of (ParsedTermsOSA X) . s & ( for s1 being Element of S st $1 in the Sorts of (ParsedTermsOSA X) . s1 holds
s <= s1 ) );
A1: for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S₁[t] ) holds
S₁[nt -tree ts]

let nt be Symbol of (DTConOSA X); :: thesis:
let ts be FinSequence of TS (DTConOSA X); :: thesis:
assume that
A2: nt ==> roots ts and
for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S₁[t] ; :: thesis:
consider o being OperSymbol of S such that
nt = [o, the carrier of S] and
ts in Args (o,(ParsedTermsOSA X)) and
nt -tree ts = (Den (o,(ParsedTermsOSA X))) . ts and
A3: for s1 being Element of S holds
( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) by A2, Th12;
reconsider s = the_result_sort_of o as SortSymbol of S ;
take s ; :: thesis:
thus ( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s & ( for s1 being Element of S st nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 holds
s <= s1 ) ) by A3; :: thesis:

end;

let sy be Symbol of (DTConOSA X); :: thesis:
assume sy in Terminals (DTConOSA X) ; :: thesis:
then consider s being Element of S, x being set such that
A5: x in X . s and
A6: sy = [x,s] by Th4;
reconsider s = s as SortSymbol of S ;
take s ; :: thesis:
thus ( root-tree sy in the Sorts of (ParsedTermsOSA X) . s & ( for s1 being Element of S st root-tree sy in the Sorts of (ParsedTermsOSA X) . s1 holds
s <= s1 ) ) by A5, A6, Th10; :: thesis:

end;

for t being DecoratedTree of the carrier of (DTConOSA X) st t in TS (DTConOSA X) holds
S₁[t] from DTCONSTR:sch 7(A4, A1);
hence ex b₁ being SortSymbol of S st
( t in the Sorts of (ParsedTermsOSA X) . b₁ & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b₁ <= s1 ) ) ; :: thesis: