set V = the Z_Module;
take (0). the Z_Module ; :: thesis: (0). the Z_Module is torsion
thus (0). the Z_Module is torsion ; :: thesis: verum