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

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

hence
LAp R2 cc= LAp R1
by A5, A0, ALTCAT_2:def 1; :: thesis: verum
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

end;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

hence
(LAp R2) . x c= (LAp R1) . x
by A3, ROUGHS_2:def 10; :: thesis: verum
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;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