let S be locally_directed OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
let s be Element of S; :: thesis:
let t be Element of TS (DTConOSA X); :: thesis:
set PTA = ParsedTermsOSA X;
set D = DTConOSA X;
set R = PTCongruence X;
reconsider y = t as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort t) by Def12;
let x, x1 be set ; :: thesis:
assume that
A1: x in X . s and
A2: t = root-tree [x,s] ; :: thesis:
A3: [x,s] in Terminals (DTConOSA X) by A1, Th4;
then reconsider sy = [x,s] as Symbol of (DTConOSA X) ;
A4: OSClass ((PTCongruence X),t) = OSClass ((PTCongruence X),y) by Def27
.= proj1 ((PTClasses X) . y) by Th25 ;
A5: (PTClasses X) . (root-tree sy) = @ sy by A3, Def21
.= { [(root-tree sy),s1] where s1 is Element of S : ex s2 being Element of S ex x2 being set st
( x2 in X . s2 & sy = [x2,s2] & s2 <= s1 ) } ;

assume x1 in OSClass ((PTCongruence X),t) ; :: thesis:
then consider z being object such that
A6: [x1,z] in (PTClasses X) . y by A4, XTUPLE_0:def 12;
ex s1 being Element of S st
( [x1,z] = [(root-tree sy),s1] & ex s2 being Element of S ex x2 being set st
( x2 in X . s2 & sy = [x2,s2] & s2 <= s1 ) ) by A2, A5, A6;
hence x1 = t by A2, XTUPLE_0:1; :: thesis:

end;