let R1, R2 be non empty RelStr ; :: thesis: ( the carrier of R1 = the carrier of R2 implies ( LAp R1 = LAp R2 iff the InternalRel of R1 = the InternalRel of R2 ) )
assume A1: the carrier of R1 = the carrier of R2 ; :: thesis: ( LAp R1 = LAp R2 iff the InternalRel of R1 = the InternalRel of R2 )
hence ( LAp R1 = LAp R2 implies the InternalRel of R1 = the InternalRel of R2 ) by Corr4; :: thesis: ( the InternalRel of R1 = the InternalRel of R2 implies LAp R1 = LAp R2 )
assume the InternalRel of R1 = the InternalRel of R2 ; :: thesis: LAp R1 = LAp 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 (LAp R1) . x = (LAp R2) . x
proof
let x be Subset of R1; :: thesis: (LAp R1) . x = (LAp R2) . x
reconsider xx = x as Subset of R2 by A1;
(LAp R1) . x = LAp x by ROUGHS_2:def 10
.= LAp xx by A2, Pom2
.= (LAp R2) . x by ROUGHS_2:def 10 ;
hence (LAp R1) . x = (LAp R2) . x ; :: thesis: verum
end;
hence LAp R1 = LAp R2 by FUNCT_2:63, A1; :: thesis: verum