let S be locally_directed OrderSortedSign; :: thesis: for X being non-empty 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 non-empty 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 Def27
.= Class ((CompClass (R1,(CComp (LeastSort t)))),xa) ;
let x be object ; :: 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: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; :: thesis: verum