theorem Th57: :: YELLOW_0:57

for L being RelStr
for S1, S2 being full SubRelStr of L st the carrier of S1 = the carrier of S2 holds
RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #)