let R1, R2 be non empty RelStr ; :: thesis: ( the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 implies LAp R2 cc= LAp R1 )
assume A0: ( the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 ) ; :: thesis: LAp R2 cc= LAp R1
A5: dom (LAp R1) = bool the carrier of R1 by FUNCT_2:def 1;
for x being set st x in dom (LAp R2) holds
(LAp R2) . x c= (LAp R1) . x

proof

let x be set ; :: thesis: ( x in dom (LAp R2) implies (LAp R2) . x c= (LAp R1) . x )
assume A2: x in dom (LAp R2) ; :: thesis: (LAp R2) . x c= (LAp R1) . x
then reconsider x1 = x as Subset of R1 by A0;
A3: (LAp R1) . x = LAp x1 by ROUGHS_2:def 10;
reconsider x2 = x as Subset of R2 by A2;
LAp x2 c= LAp x1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in LAp x2 or y in LAp x1 )
assume y in LAp x2 ; :: thesis: y in LAp x1
then y in { x where x is Element of R2 : Class ( the InternalRel of R2,x) c= x2 } by ROUGHS_1:def 4;
then consider xx being Element of R2 such that
C1: ( xx = y & Class ( the InternalRel of R2,xx) c= x2 ) ;
reconsider xxx = xx as Element of R2 ;
Class ( the InternalRel of R1,xx) c= Class ( the InternalRel of R2,xx) by RELAT_1:124, A0;
then C2: Class ( the InternalRel of R1,xx) c= x1 by C1, XBOOLE_1:1;
reconsider xx1 = xx as Element of R1 by A0;
xx1 in { x where x is Element of R1 : Class ( the InternalRel of R1,x) c= x1 } by C2;
hence y in LAp x1 by C1, ROUGHS_1:def 4; :: thesis: verum

end;

hence (LAp R2) . x c= (LAp R1) . x by A3, ROUGHS_2:def 10; :: thesis: verum

end;

hence LAp R2 cc= LAp R1 by A5, A0, ALTCAT_2:def 1; :: thesis: verum