ex v being Vector of V st
( not v is zero & v is torsion )

proof

assume B1: for v being Vector of V holds
( v is zero or not v is torsion ) ; :: thesis: contradiction
for v being Vector of V st v <> 0. V holds
not v is torsion

proof

let v be Vector of V; :: thesis: ( v <> 0. V implies not v is torsion )
assume C1: v <> 0. V ; :: thesis: not v is torsion
not v is zero by C1;
hence not v is torsion by B1; :: thesis: verum

end;

then V is torsion-free ;
hence contradiction ; :: thesis: verum

end;

then consider v being Vector of V such that
A1: ( not v is zero & v is torsion ) ;
take v ; :: thesis: ( not v is zero & v is torsion )
thus ( not v is zero & v is torsion ) by A1; :: thesis: verum