let S be OrderSortedSign; :: thesis: for X being V5 ManySortedSet of S
for t being Element of TS (DTConOSA X) ex s being SortSymbol of S st
( t in the Sorts of (ParsedTermsOSA X) . s & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s <= s1 ) )
let X be V5 ManySortedSet of S; :: thesis: for t being Element of TS (DTConOSA X) ex s being SortSymbol of S st
( t in the Sorts of (ParsedTermsOSA X) . s & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s <= s1 ) )
let t be Element of TS (DTConOSA X); :: thesis: ex s being SortSymbol of S st
( t in the Sorts of (ParsedTermsOSA X) . s & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s <= s1 ) )
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 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 A2: sy in Terminals (DTConOSA X) ; :: thesis: S₁[ root-tree sy]
consider s being Element of S, x being set such that
A3: ( x in X . s & sy = [x,s] ) by A2, 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 A3, Th10; :: thesis: verum

end;

A4: 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
A5: 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] & ts in Args o,(ParsedTermsOSA X) & nt -tree ts = (Den o,(ParsedTermsOSA X)) . ts ) and
A6: 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 A5, 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 A6; :: 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(A1, A4);
hence ex s being SortSymbol of S st
( t in the Sorts of (ParsedTermsOSA X) . s & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s <= s1 ) ) ; :: thesis: verum