let R1, R2 be non empty RelStr ; :: thesis: ( the carrier of R1 = the carrier of R2 & UAp R1 cc= UAp R2 implies the InternalRel of R1 c= the InternalRel of R2 )

assume T0: the carrier of R1 = the carrier of R2 ; :: thesis: ( not UAp R1 cc= UAp R2 or the InternalRel of R1 c= the InternalRel of R2 )

assume XX: UAp R1 cc= UAp R2 ; :: thesis: the InternalRel of R1 c= the InternalRel of R2

set U1 = UAp R1;

set U2 = UAp R2;

set A = the carrier of R1;

for x, y being object st [x,y] in the InternalRel of R1 holds

[x,y] in the InternalRel of R2

assume T0: the carrier of R1 = the carrier of R2 ; :: thesis: ( not UAp R1 cc= UAp R2 or the InternalRel of R1 c= the InternalRel of R2 )

assume XX: UAp R1 cc= UAp R2 ; :: thesis: the InternalRel of R1 c= the InternalRel of R2

set U1 = UAp R1;

set U2 = UAp R2;

set A = the carrier of R1;

for x, y being object st [x,y] in the InternalRel of R1 holds

[x,y] in the InternalRel of R2

proof

hence
the InternalRel of R1 c= the InternalRel of R2
by RELAT_1:def 3; :: thesis: verum
let x, y be object ; :: thesis: ( [x,y] in the InternalRel of R1 implies [x,y] in the InternalRel of R2 )

assume B0: [x,y] in the InternalRel of R1 ; :: thesis: [x,y] in the InternalRel of R2

then b0: ( x in the carrier of R1 & y in the carrier of R1 ) by ZFMISC_1:87;

reconsider xx = x, yy = y as Element of R1 by B0, ZFMISC_1:87;

b1: dom (UAp R1) = bool the carrier of R1 by FUNCT_2:def 1;

{y} c= the carrier of R1 by ZFMISC_1:31, b0;

then B1: (UAp R1) . {y} c= (UAp R2) . {y} by XX, ALTCAT_2:def 1, b1;

reconsider yyy = {yy} as Subset of R2 by T0;

reconsider yy1 = {yy} as Subset of R1 ;

xx in UAp yy1 by Th5A, B0;

then xx in (UAp R1) . {yy} by ROUGHS_2:def 11;

then x in (UAp R2) . {y} by B1;

then xx in UAp yyy by ROUGHS_2:def 11;

hence [x,y] in the InternalRel of R2 by ROUGHS_2:5, T0; :: thesis: verum

end;assume B0: [x,y] in the InternalRel of R1 ; :: thesis: [x,y] in the InternalRel of R2

then b0: ( x in the carrier of R1 & y in the carrier of R1 ) by ZFMISC_1:87;

reconsider xx = x, yy = y as Element of R1 by B0, ZFMISC_1:87;

b1: dom (UAp R1) = bool the carrier of R1 by FUNCT_2:def 1;

{y} c= the carrier of R1 by ZFMISC_1:31, b0;

then B1: (UAp R1) . {y} c= (UAp R2) . {y} by XX, ALTCAT_2:def 1, b1;

reconsider yyy = {yy} as Subset of R2 by T0;

reconsider yy1 = {yy} as Subset of R1 ;

xx in UAp yy1 by Th5A, B0;

then xx in (UAp R1) . {yy} by ROUGHS_2:def 11;

then x in (UAp R2) . {y} by B1;

then xx in UAp yyy by ROUGHS_2:def 11;

hence [x,y] in the InternalRel of R2 by ROUGHS_2:5, T0; :: thesis: verum