theorem Th17: :: WSIERP_1:17

for k, l being Integer st k <> 0 holds
( k divides l iff l / k is Integer )