theorem Corr4: :: ROUGHS_3:53

for R1, R2 being non empty RelStr st the carrier of R1 = the carrier of R2 & LAp R1 = LAp R2 holds
the InternalRel of R2 = the InternalRel of R1