let S be locally_directed OrderSortedSign; for X being V2() 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 V2() 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 R be 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 t1, t2 be Element of TS (DTConOSA X); ( 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 ( OSClass (R,t1) = OSClass (R,t2) implies t2 in OSClass (R,t1) )
assume
t2 in OSClass (
R,
t1)
;
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
;
verum
end;
assume
OSClass (R,t1) = OSClass (R,t2)
; t2 in OSClass (R,t1)
hence
t2 in OSClass (R,t1)
by Th32; verum