theorem :: NAT_D:56

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