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

assume A1: the carrier of R1 = the carrier of R2 ; :: thesis: ( UAp R1 = UAp R2 iff the InternalRel of R1 = the InternalRel of R2 )

hence ( UAp R1 = UAp R2 implies the InternalRel of R1 = the InternalRel of R2 ) by Corr3A; :: thesis: ( the InternalRel of R1 = the InternalRel of R2 implies UAp R1 = UAp R2 )

assume the InternalRel of R1 = the InternalRel of R2 ; :: thesis: UAp R1 = UAp R2

then A2: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) by A1;

for x being Subset of R1 holds (UAp R1) . x = (UAp R2) . x

assume A1: the carrier of R1 = the carrier of R2 ; :: thesis: ( UAp R1 = UAp R2 iff the InternalRel of R1 = the InternalRel of R2 )

hence ( UAp R1 = UAp R2 implies the InternalRel of R1 = the InternalRel of R2 ) by Corr3A; :: thesis: ( the InternalRel of R1 = the InternalRel of R2 implies UAp R1 = UAp R2 )

assume the InternalRel of R1 = the InternalRel of R2 ; :: thesis: UAp R1 = UAp R2

then A2: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) by A1;

for x being Subset of R1 holds (UAp R1) . x = (UAp R2) . x

proof

hence
UAp R1 = UAp R2
by FUNCT_2:63, A1; :: thesis: verum
let x be Subset of R1; :: thesis: (UAp R1) . x = (UAp R2) . x

reconsider xx = x as Subset of R2 by A1;

(UAp R1) . x = UAp x by ROUGHS_2:def 11

.= UAp xx by A2, Pom1

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

hence (UAp R1) . x = (UAp R2) . x ; :: thesis: verum

end;reconsider xx = x as Subset of R2 by A1;

(UAp R1) . x = UAp x by ROUGHS_2:def 11

.= UAp xx by A2, Pom1

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

hence (UAp R1) . x = (UAp R2) . x ; :: thesis: verum