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

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

hence
LAp R1 = LAp R2
by FUNCT_2:63, A1; :: thesis: verum
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;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