theorem :: INT_1:62

for n being Integer st n > 0 holds
for a being Integer holds
( a mod n = 0 iff n divides a )