let S be OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
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 non-empty ManySortedSet of S; :: 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 t = [x,s] as Terminal of (DTConOSA X) by A1, Th4;
reconsider s0 = s, s11 = s1 as Element of S ;
reconsider SPTA = the Sorts of (ParsedTermsOSA X) as OrderSortedSet of S ;
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 ) )
thus A2: 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]) . {}
assume A3: [z, the carrier of S] = (root-tree [x,s]) . {} ; :: thesis: contradiction
(root-tree [x,s]) . {} = [x,s] by TREES_4:3;
then s = the carrier of S by A3, XTUPLE_0:1;
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 object 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
A4: a = root-tree [x,s] and
A5: ( ex s2 being Element of S ex x being object 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
A6: s2 <= s1 and
x1 in X . s2 and
A7: a = root-tree [x1,s2] by A2, A4, A5;
[x1,s2] = [x,s] by A4, A7, TREES_4:4;
hence s <= s1 by A6, XTUPLE_0:1; :: thesis: verum

end;

assume s <= s1 ; :: thesis: root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1
then A8: SPTA . s0 c= SPTA . s11 by OSALG_1:def 16;
root-tree t in { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object 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 root-tree [x,s] in SPTA . s0 by Th9;
hence root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 by A8; :: thesis: verum