theorem Th3: :: NAT_D:3

for i, j being natural Number holds
( j divides i iff i = j * (i div j) )