set V = the non trivial torsion-free Z_Module;
set v = the non zero Vector of the non trivial torsion-free Z_Module;
take Lin { the non zero Vector of the non trivial torsion-free Z_Module} ; :: thesis: not Lin { the non zero Vector of the non trivial torsion-free Z_Module} is trivial
the non zero Vector of the non trivial torsion-free Z_Module <> 0. the non trivial torsion-free Z_Module ;
hence not Lin { the non zero Vector of the non trivial torsion-free Z_Module} is trivial by ThTrivial2; :: thesis: verum