for i, n being Nat st i <> 0 holds
( i divides n iff n mod i = 0 )