EMbedding V is Submodule of DivisibleMod V by ThDivisible2;
hence EMbedding V is torsion-free ; :: thesis: verum