let S be locally_directed OrderSortedSign; :: thesis: for X being V5() 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 V5() ManySortedSet of S; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: OSClass R1,t c= OSClass R2,t
A2: OSClass R1,t = OSClass R1,xa by Def28
.= Class (CompClass R1,(CComp (LeastSort t))),xa ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in OSClass R1,t or x in OSClass R2,t )
assume x in OSClass R1,t ; :: thesis: x in OSClass R2,t
then [x,xa] in CompClass R1,(CComp (LeastSort t)) by A2, EQREL_1:27;
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 11;
reconsider xa = t, xb = x as Element of the Sorts of (ParsedTermsOSA X) . s1 by A3, ZFMISC_1:106;
A4: R1 . s1 c= R2 . s1 by A1, PBOOLE:def 5;
x in the Sorts of (ParsedTermsOSA X) . s1 by A3, ZFMISC_1:106;
then reconsider t1 = x as Element of TS (DTConOSA X) by Th16;
OSClass R2,t1 = OSClass R2,xb by Def28
.= OSClass R2,xa by A3, A4, OSALG_4:13
.= OSClass R2,t by Def28 ;
hence x in OSClass R2,t by Th35; :: thesis: verum