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]

proof

let nt be Symbol of (DTConOSA X); :: thesis: 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 ts be FinSequence of TS (DTConOSA X); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S₁[t] ) implies S₁[nt -tree ts] )
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: S₁[nt -tree ts]
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: ( 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 ) )
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: verum

end;

A4: for s being Symbol of (DTConOSA X) st s in Terminals (DTConOSA X) holds
S₁[ root-tree s]

proof

let sy be Symbol of (DTConOSA X); :: thesis: ( sy in Terminals (DTConOSA X) implies S₁[ root-tree sy] )
assume sy in Terminals (DTConOSA X) ; :: thesis: S₁[ root-tree sy]
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: ( 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 ) )
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: verum

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: verum