let i, j, h be natural Number ; :: thesis: ( i <> 0 & h = j * i implies j <= h )
assume i <> 0 ; :: thesis: ( not h = j * i or j <= h )
then consider k being Nat such that
A1: i = k + 1 by Th6;
assume h = j * i ; :: thesis: j <= h
then h = (j * k) + (j * 1) by A1;
hence j <= h by Th11; :: thesis: verum