let S be locally_directed OrderSortedSign; :: thesis: for X being V16() 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 V16() 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 Def28
.= 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:27;
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 11;
reconsider x11 = x1, x22 = t2 as Element of the Sorts of (ParsedTermsOSA X) . s2 by A2, ZFMISC_1:106;
thus OSClass R,t1 = OSClass R,x11 by Def28
.= OSClass R,x22 by A2, OSALG_4:13
.= OSClass R,t2 by Def28 ; :: thesis: verum

end;

assume OSClass R,t1 = OSClass R,t2 ; :: thesis: t2 in OSClass R,t1
hence t2 in OSClass R,t1 by Th33; :: thesis: verum