let V be non torsion-free Z_Module; :: thesis: not V is trivial
assume V is trivial ; :: thesis: contradiction
then (Omega). V = (0). V by ThTrivial1;
hence contradiction by ThTFX; :: thesis: verum