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 UAp R1 cc= UAp R2 )

assume A0: ( the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 ) ; :: thesis: UAp R1 cc= UAp R2

a1: dom (UAp R2) = bool the carrier of R2 by FUNCT_2:def 1;

for x being set st x in dom (UAp R1) holds

(UAp R1) . x c= (UAp R2) . x

assume A0: ( the carrier of R1 = the carrier of R2 & the InternalRel of R1 c= the InternalRel of R2 ) ; :: thesis: UAp R1 cc= UAp R2

a1: dom (UAp R2) = bool the carrier of R2 by FUNCT_2:def 1;

for x being set st x in dom (UAp R1) holds

(UAp R1) . x c= (UAp R2) . x

proof

hence
UAp R1 cc= UAp R2
by a1, A0, ALTCAT_2:def 1; :: thesis: verum
let x be set ; :: thesis: ( x in dom (UAp R1) implies (UAp R1) . x c= (UAp R2) . x )

assume A2: x in dom (UAp R1) ; :: thesis: (UAp R1) . x c= (UAp R2) . x

then reconsider x1 = x as Subset of R1 ;

reconsider x2 = x as Subset of R2 by A0, A2;

A4: (UAp R2) . x = UAp x2 by ROUGHS_2:def 11;

UAp x1 c= UAp x2

end;assume A2: x in dom (UAp R1) ; :: thesis: (UAp R1) . x c= (UAp R2) . x

then reconsider x1 = x as Subset of R1 ;

reconsider x2 = x as Subset of R2 by A0, A2;

A4: (UAp R2) . x = UAp x2 by ROUGHS_2:def 11;

UAp x1 c= UAp x2

proof

hence
(UAp R1) . x c= (UAp R2) . x
by ROUGHS_2:def 11, A4; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in UAp x1 or y in UAp x2 )

assume y in UAp x1 ; :: thesis: y in UAp x2

then y in { x where x is Element of R1 : Class ( the InternalRel of R1,x) meets x1 } by ROUGHS_1:def 5;

then consider xx being Element of R1 such that

C1: ( xx = y & Class ( the InternalRel of R1,xx) meets x1 ) ;

reconsider xxx = xx as Element of R2 by A0;

consider z being object such that

C2: ( z in Class ( the InternalRel of R1,xx) & z in x1 ) by C1, XBOOLE_0:3;

Class ( the InternalRel of R1,xx) c= Class ( the InternalRel of R2,xx) by RELAT_1:124, A0;

then Class ( the InternalRel of R2,xx) meets x2 by C2, XBOOLE_0:3;

then xxx in { x where x is Element of R2 : Class ( the InternalRel of R2,x) meets x2 } ;

hence y in UAp x2 by C1, ROUGHS_1:def 5; :: thesis: verum

end;assume y in UAp x1 ; :: thesis: y in UAp x2

then y in { x where x is Element of R1 : Class ( the InternalRel of R1,x) meets x1 } by ROUGHS_1:def 5;

then consider xx being Element of R1 such that

C1: ( xx = y & Class ( the InternalRel of R1,xx) meets x1 ) ;

reconsider xxx = xx as Element of R2 by A0;

consider z being object such that

C2: ( z in Class ( the InternalRel of R1,xx) & z in x1 ) by C1, XBOOLE_0:3;

Class ( the InternalRel of R1,xx) c= Class ( the InternalRel of R2,xx) by RELAT_1:124, A0;

then Class ( the InternalRel of R2,xx) meets x2 by C2, XBOOLE_0:3;

then xxx in { x where x is Element of R2 : Class ( the InternalRel of R2,x) meets x2 } ;

hence y in UAp x2 by C1, ROUGHS_1:def 5; :: thesis: verum