let x be Divisor of n; :: thesis: x is n _or_smaller
consider k being Integer such that
A1: x * k = n by Def2, INT_1:def 3;
k >= 0 by A1;
then reconsider k = k as Element of NAT by INT_1:3;
k <> 0 by A1;
hence x is n _or_smaller by A1, NAT_1:24; :: thesis: verum