let i, j be Nat; :: thesis: ( i divides j & j divides i implies i = j )
assume i divides j ; :: thesis: ( not j divides i or i = j )
then consider a being Integer such that
A1: j = i * a by INT_1:def 3;
assume j divides i ; :: thesis: i = j
then consider b being Integer such that
A2: i = j * b by INT_1:def 3;
( i <> 0 implies i = j )

proof

A3: i >= 0 by NAT_1:2;
assume A4: i <> 0 ; :: thesis: i = j
1 * i = i * (a * b) by A1, A2;
then a * b = 1 by A4, XCMPLX_1:5;
then ( i = j * 1 or i = j * (- 1) ) by A2, INT_1:9;
hence i = j by A4, A3; :: thesis: verum

end;

hence i = j by A1; :: thesis: verum