theorem :: ZMODUL06:16

for V being torsion-free Z_Module
for v being Vector of V holds
( v is torsion iff v = 0. V ) by defTorsionFree;