let S be locally_directed OrderSortedSign; for X being V2() ManySortedSet of S
for R1, R2 being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) st R1 c= R2 holds
OSClass (R1,t) c= OSClass (R2,t)
let X be V2() ManySortedSet of S; for R1, R2 being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) st R1 c= R2 holds
OSClass (R1,t) c= OSClass (R2,t)
let R1, R2 be OSCongruence of ParsedTermsOSA X; for t being Element of TS (DTConOSA X) st R1 c= R2 holds
OSClass (R1,t) c= OSClass (R2,t)
let t be Element of TS (DTConOSA X); ( R1 c= R2 implies OSClass (R1,t) c= OSClass (R2,t) )
set s = LeastSort t;
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set D = DTConOSA X;
set CC1 = CComp (LeastSort t);
set CR1 = CompClass (R1,(CComp (LeastSort t)));
reconsider xa = t as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort t) by Def12;
assume A1:
R1 c= R2
; OSClass (R1,t) c= OSClass (R2,t)
A2: OSClass (R1,t) =
OSClass (R1,xa)
by Def27
.=
Class ((CompClass (R1,(CComp (LeastSort t)))),xa)
;
let x be object ; TARSKI:def 3 ( not x in OSClass (R1,t) or x in OSClass (R2,t) )
assume
x in OSClass (R1,t)
; x in OSClass (R2,t)
then
[x,xa] in CompClass (R1,(CComp (LeastSort t)))
by A2, EQREL_1:19;
then consider s1 being Element of S such that
s1 in CComp (LeastSort t)
and
A3:
[x,xa] in R1 . s1
by OSALG_4:def 9;
reconsider xa = t, xb = x as Element of the Sorts of (ParsedTermsOSA X) . s1 by A3, ZFMISC_1:87;
A4:
R1 . s1 c= R2 . s1
by A1;
x in the Sorts of (ParsedTermsOSA X) . s1
by A3, ZFMISC_1:87;
then reconsider t1 = x as Element of TS (DTConOSA X) by Th15;
OSClass (R2,t1) =
OSClass (R2,xb)
by Def27
.=
OSClass (R2,xa)
by A3, A4, OSALG_4:12
.=
OSClass (R2,t)
by Def27
;
hence
x in OSClass (R2,t)
by Th34; verum