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 9;
assume j divides i ; :: thesis: i = j
then consider b being Integer such that
A2: i = j * b by INT_1:def 9;
( i <> 0 implies i = j )

proof

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

end;

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