let j, i be Nat; :: thesis: ( 0 < j & i divides j implies i <= j )
assume A1: ( 0 < j & i divides j ) ; :: thesis: i <= j
then A2: j = i * (j div i) by Th3;
then j div i <> 0 by A1;
then consider m being Nat such that
A3: j div i = m + 1 by NAT_1:6;
i * (m + 1) = i + (i * m) ;
hence i <= j by A2, A3, NAT_1:11; :: thesis: verum