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