:: deftheorem defTorsionFree defines torsion-free ZMODUL06:def 3 :
for V being Z_Module holds
( V is torsion-free iff for v being Vector of V st v <> 0. V holds
not v is torsion );