let S be locally_directed OrderSortedSign; :: thesis:
let X be V5() ManySortedSet of ; :: 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;
A1: OSClass (PTCongruence X),t = OSClass (PTCongruence X),y by Def28
.= proj1 ((PTClasses X) . y) by Th26 ;
let x, x1 be set ; :: thesis:
assume A2: ( x in X . s & t = root-tree [x,s] ) ; :: thesis:
A3: [x,s] in Terminals (DTConOSA X) by A2, Th4;
then reconsider sy = [x,s] as Symbol of (DTConOSA X) ;
A4: (PTClasses X) . (root-tree sy) = @ sy by A3, Def22
.= { [(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 ) } ;

hereby :: thesis:

assume x1 in OSClass (PTCongruence X),t ; :: thesis:
then consider z being set such that
A5: [x1,z] in (PTClasses X) . y by A1, RELAT_1:def 4;
consider s1 being Element of S such that
A6: [x1,z] = [(root-tree sy),s1] and
ex s2 being Element of S ex x2 being set st
( x2 in X . s2 & sy = [x2,s2] & s2 <= s1 ) by A2, A4, A5;
thus x1 = t by A2, A6, ZFMISC_1:33; :: thesis:

end;

assume x1 = t ; :: thesis:
then [x1,s] in (PTClasses X) . y by A2, A4;
hence x1 in OSClass (PTCongruence X),t by A1, RELAT_1:def 4; :: thesis: