let i, j be natural Number ; :: thesis: ( i divides j & j divides i implies i = j )
assume that
A1: i divides j and
A2: j divides i ; :: thesis: i = j
A3: j = i * (j div i) by A1, Th3;
i = j * (i div j) by A2, Th3;
then A4: i * 1 = (i * (j div i)) * (i div j) by A3
.= i * ((j div i) * (i div j)) ;
A5: ( i = 0 implies i = j ) by A3;
( (j div i) * (i div j) = 1 implies i = j )

proof

assume (j div i) * (i div j) = 1 ; :: thesis: i = j
then j div i = 1 by NAT_1:15;
hence i = j by A3; :: thesis: verum

end;

hence i = j by A4, A5, XCMPLX_1:5; :: thesis: verum