theorem ThTV6: :: ZMODUL06:9

for V being Z_Module
for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
( v is torsion iff w is torsion )