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