theorem ThDivisible2: :: ZMODUL08:24

for V being torsion-free Z_Module holds EMbedding V is Submodule of DivisibleMod V