let S be locally_directed OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s holds OSClass ((PTCongruence X),x) = proj1 ((PTClasses X) . x)
let X be non-empty ManySortedSet of S; :: thesis: for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s holds OSClass ((PTCongruence X),x) = proj1 ((PTClasses X) . x)
let s be Element of S; :: thesis: for x being Element of the Sorts of (ParsedTermsOSA X) . s holds OSClass ((PTCongruence X),x) = proj1 ((PTClasses X) . x)
let x be Element of the Sorts of (ParsedTermsOSA X) . s; :: thesis: OSClass ((PTCongruence X),x) = proj1 ((PTClasses X) . x)
set R = PTCongruence X;
set PTA = ParsedTermsOSA X;
set D = DTConOSA X;
for z being object holds
( z in OSClass ((PTCongruence X),x) iff z in proj1 ((PTClasses X) . x) )

proof

let z be object ; :: thesis: ( z in OSClass ((PTCongruence X),x) iff z in proj1 ((PTClasses X) . x) )

hereby :: thesis: ( z in proj1 ((PTClasses X) . x) implies z in OSClass ((PTCongruence X),x) )

assume z in OSClass ((PTCongruence X),x) ; :: thesis: z in proj1 ((PTClasses X) . x)
then [z,x] in CompClass ((PTCongruence X),(CComp s)) by EQREL_1:19;
then ex s1 being Element of S st
( s1 in CComp s & [z,s1] in (PTClasses X) . x ) by Th24;
hence z in proj1 ((PTClasses X) . x) by XTUPLE_0:def 12; :: thesis: verum

end;

assume z in proj1 ((PTClasses X) . x) ; :: thesis: z in OSClass ((PTCongruence X),x)
then consider s1 being object such that
A1: [z,s1] in (PTClasses X) . x by XTUPLE_0:def 12;
reconsider s2 = s1 as Element of S by A1, Th23;
reconsider x1 = x, z1 = z as Element of TS (DTConOSA X) by A1, Th23;
A2: LeastSort x1 <= s by Def12;
[z1,s2] in (PTClasses X) . x1 by A1;
then [x1,s2] in (PTClasses X) . x1 by Th20;
then x in the Sorts of (ParsedTermsOSA X) . s1 by Th19;
then LeastSort x1 <= s2 by Def12;
then CComp s2 = CComp (LeastSort x1) by OSALG_4:4
.= CComp s by A2, OSALG_4:4 ;
then s2 in CComp s by EQREL_1:20;
then [z,x] in CompClass ((PTCongruence X),(CComp s)) by A1, Th24;
hence z in OSClass ((PTCongruence X),x) by EQREL_1:19; :: thesis: verum

end;

hence OSClass ((PTCongruence X),x) = proj1 ((PTClasses X) . x) by TARSKI:2; :: thesis: verum