let S be locally_directed OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
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 V5() ManySortedSet of ; :: 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 set holds
( z in OSClass (PTCongruence X),x iff z in proj1 ((PTClasses X) . x) )
proof
let z be
set ;
:: thesis: ( z in OSClass (PTCongruence X),x iff z in proj1 ((PTClasses X) . x) )
assume
z in proj1 ((PTClasses X) . x)
;
:: thesis: z in OSClass (PTCongruence X),x
then consider s1 being
set such that A2:
[z,s1] in (PTClasses X) . x
by RELAT_1:def 4;
reconsider x1 =
x,
z1 =
z as
Element of
TS (DTConOSA X) by A2, Th24;
reconsider s2 =
s1 as
Element of
S by A2, Th24;
[z1,s2] in (PTClasses X) . x1
by A2;
then
[x1,s2] in (PTClasses X) . x1
by Th21;
then
x in the
Sorts of
(ParsedTermsOSA X) . s1
by Th20;
then A3:
(
LeastSort x1 <= s2 &
LeastSort x1 <= s )
by Def12;
then CComp s2 =
CComp (LeastSort x1)
by OSALG_4:5
.=
CComp s
by A3, OSALG_4:5
;
then
s2 in CComp s
by EQREL_1:28;
then
[z,x] in CompClass (PTCongruence X),
(CComp s)
by A2, Th25;
hence
z in OSClass (PTCongruence X),
x
by EQREL_1:27;
:: thesis: verum
end;
hence
OSClass (PTCongruence X),x = proj1 ((PTClasses X) . x)
by TARSKI:2; :: thesis: verum