let S be OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
for s, s1 being Element of S
for x being set st x in X . s holds
( root-tree [x,s] is Element of TS (DTConOSA X) & ( for z being set holds [z,the carrier of S] <> (root-tree [x,s]) . {} ) & ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
let X be V5() ManySortedSet of ; :: thesis: for s, s1 being Element of S
for x being set st x in X . s holds
( root-tree [x,s] is Element of TS (DTConOSA X) & ( for z being set holds [z,the carrier of S] <> (root-tree [x,s]) . {} ) & ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
let s, s1 be Element of S; :: thesis: for x being set st x in X . s holds
( root-tree [x,s] is Element of TS (DTConOSA X) & ( for z being set holds [z,the carrier of S] <> (root-tree [x,s]) . {} ) & ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
let x be set ; :: thesis: ( x in X . s implies ( root-tree [x,s] is Element of TS (DTConOSA X) & ( for z being set holds [z,the carrier of S] <> (root-tree [x,s]) . {} ) & ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) ) )
assume A1: x in X . s ; :: thesis: ( root-tree [x,s] is Element of TS (DTConOSA X) & ( for z being set holds [z,the carrier of S] <> (root-tree [x,s]) . {} ) & ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
set PTA = ParsedTermsOSA X;
set D = DTConOSA X;
reconsider s0 = s, s11 = s1 as Element of S ;
reconsider SPTA = the Sorts of (ParsedTermsOSA X) as OrderSortedSet of ;
reconsider t = [x,s] as Terminal of (DTConOSA X) by A1, Th4;
root-tree t is Element of TS (DTConOSA X) ;
hence root-tree [x,s] is Element of TS (DTConOSA X) ; :: thesis: ( ( for z being set holds [z,the carrier of S] <> (root-tree [x,s]) . {} ) & ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
root-tree t in { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } by A1;
then A2: root-tree [x,s] in SPTA . s0 by Th9;
thus A3: for z being set holds [z,the carrier of S] <> (root-tree [x,s]) . {} :: thesis: ( ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )

proof

let z be set ; :: thesis: [z,the carrier of S] <> (root-tree [x,s]) . {}
A4: (root-tree [x,s]) . {} = [x,s] by TREES_4:3;
assume [z,the carrier of S] = (root-tree [x,s]) . {} ; :: thesis: contradiction
then s = the carrier of S by A4, ZFMISC_1:33;
then s in s ;
hence contradiction ; :: thesis: verum

end;

hereby :: thesis: ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 )

assume root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ; :: thesis: s <= s1
then root-tree [x,s] in { a where a is Element of TS (DTConOSA X) : ( ex s2 being Element of S ex x being set st
( s2 <= s1 & x in X . s2 & a = root-tree [x,s2] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s1 ) ) } by Th9;
then consider a being Element of TS (DTConOSA X) such that
A5: a = root-tree [x,s] and
A6: ( ex s2 being Element of S ex x being set st
( s2 <= s1 & x in X . s2 & a = root-tree [x,s2] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s1 ) ) ;
consider s2 being Element of S, x1 being set such that
A7: ( s2 <= s1 & x1 in X . s2 & a = root-tree [x1,s2] ) by A3, A5, A6;
[x1,s2] = [x,s] by A5, A7, TREES_4:4;
hence s <= s1 by A7, ZFMISC_1:33; :: thesis: verum

end;

assume s <= s1 ; :: thesis: root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1
then SPTA . s0 c= SPTA . s11 by OSALG_1:def 18;
hence root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 by A2; :: thesis: verum