theorem :: NAT_D:57

for k, i, j being natural Number st i < j & k < j holds
i -' k < j -' k