let R1, R2 be non empty RelStr ; :: thesis:
assume A0: ( the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 ) ; :: thesis:
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

let x be set ; :: thesis:
assume A2: x in dom (LAp R2) ; :: thesis:
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

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in LAp x2 ; :: thesis:
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:

end;

end;