let S be locally_directed OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for R being OSCongruence of ParsedTermsOSA X
for t1, t2 being Element of TS (DTConOSA X) holds
( t2 in OSClass (R,t1) iff OSClass (R,t1) = OSClass (R,t2) )
let X be non-empty ManySortedSet of S; :: thesis: for R being OSCongruence of ParsedTermsOSA X
for t1, t2 being Element of TS (DTConOSA X) holds
( t2 in OSClass (R,t1) iff OSClass (R,t1) = OSClass (R,t2) )
let R be OSCongruence of ParsedTermsOSA X; :: thesis: for t1, t2 being Element of TS (DTConOSA X) holds
( t2 in OSClass (R,t1) iff OSClass (R,t1) = OSClass (R,t2) )
let t1, t2 be Element of TS (DTConOSA X); :: thesis: ( t2 in OSClass (R,t1) iff OSClass (R,t1) = OSClass (R,t2) )
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
reconsider x1 = t1 as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort t1) by Def12;
set CC1 = CComp (LeastSort t1);
set CR1 = CompClass (R,(CComp (LeastSort t1)));
A1: OSClass (R,t1) = OSClass (R,x1) by Def27
.= Class ((CompClass (R,(CComp (LeastSort t1)))),x1) ;

hereby :: thesis: ( OSClass (R,t1) = OSClass (R,t2) implies t2 in OSClass (R,t1) )

assume t2 in OSClass (R,t1) ; :: thesis: OSClass (R,t1) = OSClass (R,t2)
then [t2,x1] in CompClass (R,(CComp (LeastSort t1))) by A1, EQREL_1:19;
then consider s2 being Element of S such that
s2 in CComp (LeastSort t1) and
A2: [t2,x1] in R . s2 by OSALG_4:def 9;
reconsider x11 = x1, x22 = t2 as Element of the Sorts of (ParsedTermsOSA X) . s2 by A2, ZFMISC_1:87;
thus OSClass (R,t1) = OSClass (R,x11) by Def27
.= OSClass (R,x22) by A2, OSALG_4:12
.= OSClass (R,t2) by Def27 ; :: thesis: verum

end;

assume OSClass (R,t1) = OSClass (R,t2) ; :: thesis: t2 in OSClass (R,t1)
hence t2 in OSClass (R,t1) by Th32; :: thesis: verum