let V be non trivial torsion-free Z_Module; :: thesis: not V is torsion
(Omega). V <> (0). V ;
then consider v being Vector of V such that
A2: ( v in (Omega). V & v <> 0. V ) by ZMODUL04:24;
thus not V is torsion by A2, defTorsionFree; :: thesis: verum