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