theorem Th32: :: WAYBEL_1:32

for L being non empty RelStr
for f being Function of L,L holds (inclusion f) * (corestr f) = f