set X = { v where v is Vector of V : v is torsion } ;
A1: for x being object st x in { v where v is Vector of V : v is torsion } holds
x in the carrier of V

proof

let x be object ; :: thesis: ( x in { v where v is Vector of V : v is torsion } implies x in the carrier of V )
assume B1: x in { v where v is Vector of V : v is torsion } ; :: thesis: x in the carrier of V
consider y being Vector of V such that
B2: ( y = x & y is torsion ) by B1;
thus x in the carrier of V by B2; :: thesis: verum

end;

A2: for x being Vector of V st x in { v where v is Vector of V : v is torsion } holds
x is torsion

proof

let x be Vector of V; :: thesis: ( x in { v where v is Vector of V : v is torsion } implies x is torsion )
assume B1: x in { v where v is Vector of V : v is torsion } ; :: thesis: x is torsion
consider y being Vector of V such that
B2: ( y = x & y is torsion ) by B1;
thus x is torsion by B2; :: thesis: verum

end;

{ v where v is Vector of V : v is torsion } c= the carrier of V by A1;
then reconsider X = { v where v is Vector of V : v is torsion } as Subset of V ;
A4: for v, u being Vector of V st v in X & u in X holds
v + u in X

proof

let v, u be Vector of V; :: thesis: ( v in X & u in X implies v + u in X )
assume B1: ( v in X & u in X ) ; :: thesis: v + u in X
( v is torsion & u is torsion ) by A2, B1;
then v + u is torsion by ZMODUL06:5;
hence v + u in X ; :: thesis: verum

end;

for i being Element of INT.Ring
for v being Vector of V st v in X holds
i * v in X

proof

let i be Element of INT.Ring; :: thesis: for v being Vector of V st v in X holds
i * v in X
let v be Vector of V; :: thesis: ( v in X implies i * v in X )
assume B1: v in X ; :: thesis: i * v in X
i * v is torsion by A2, B1, ZMODUL06:8;
hence i * v in X ; :: thesis: verum

end;

then A6: X is linearly-closed by A4;
0. V in X ;
then reconsider X = X as non empty Subset of V ;
consider W being strict Subspace of V such that
A7: X = the carrier of W by A6, ZMODUL01:50;
take W ; :: thesis: the carrier of W = { v where v is Vector of V : v is torsion }
thus the carrier of W = { v where v is Vector of V : v is torsion } by A7; :: thesis: verum