let R1, R2 be non empty RelStr ; ( 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 )
; 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
let x be
set ;
( x in dom (UAp R1) implies (UAp R1) . x c= (UAp R2) . x )
assume A2:
x in dom (UAp R1)
;
(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
let y be
object ;
TARSKI:def 3 ( not y in UAp x1 or y in UAp x2 )
assume
y in UAp x1
;
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;
verum
end;
hence
(UAp R1) . x c= (UAp R2) . x
by ROUGHS_2:def 11, A4;
verum
end;
hence
UAp R1 cc= UAp R2
by a1, A0, ALTCAT_2:def 1; verum