let x be Divisor of n; :: thesis: not x is zero
consider k being Integer such that
A1: x * k = n by Def2, INT_1:def 3;
thus not x is zero by A1; :: thesis: verum