let S be locally_directed OrderSortedSign; for X being V2() 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 V2() 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 s be 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 Element of the Sorts of (ParsedTermsOSA X) . s; 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 ;
( z in OSClass ((PTCongruence X),x) iff z in proj1 ((PTClasses X) . x) )
assume
z in proj1 ((PTClasses X) . x)
;
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;
verum
end;
hence
OSClass ((PTCongruence X),x) = proj1 ((PTClasses X) . x)
by TARSKI:2; verum