let W be Subspace of V; :: thesis: W is torsion-free
for w being Vector of W st w <> 0. W holds
not w is torsion

proof

let w be Vector of W; :: thesis: ( w <> 0. W implies not w is torsion )
assume A1: w <> 0. W ; :: thesis: not w is torsion
A2: w <> 0. V by A1, ZMODUL01:26;
reconsider v = w as Vector of V by ZMODUL01:25;
not v is torsion by A2, defTorsionFree;
hence not w is torsion by ThTV6; :: thesis: verum

end;

hence W is torsion-free ; :: thesis: verum