theorem ThDivisible3: :: ZMODUL08:32
for V being torsion-free Z_Module
for r being Element of F_Rat holds EMbedding (r,V) is Submodule of DivisibleMod V