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

proof

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;

hence UAp R1 = UAp R2 by FUNCT_2:63, A1; :: thesis: verum