let i, j be Nat; :: thesis: ( i divides j & j divides i implies i = j )
assume ( i divides j & j divides i ) ; :: thesis: i = j
then A1: ( j = i * (j div i) & i = j * (i div j) ) by Th3;
then A2: i * 1 = i * ((j div i) * (i div j)) ;
A3: ( i = 0 implies i = j ) by A1;
( (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 A1; :: thesis: verum

end;

hence i = j by A2, A3, XCMPLX_1:5; :: thesis: verum