theorem :: ZMODUL08:7

for V being Z_Module holds
( V is divisible iff (Omega). V is divisible )