theorem Lm3b: :: FIELD_15:1

for n being Nat
for m being non zero Nat holds
( n / m is Nat iff m divides n )