let R1, R2 be non empty RelStr ; ( 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
; ( not UAp R1 cc= UAp R2 or the InternalRel of R1 c= the InternalRel of R2 )
assume XX:
UAp R1 cc= UAp R2
; 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
let x,
y be
object ;
( [x,y] in the InternalRel of R1 implies [x,y] in the InternalRel of R2 )
assume B0:
[x,y] in the
InternalRel of
R1
;
[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;
verum
end;
hence
the InternalRel of R1 c= the InternalRel of R2
by RELAT_1:def 3; verum