set V = the non trivial torsion finitely-generated Z_Module;
take the non trivial torsion finitely-generated Z_Module ; :: thesis: not the non trivial torsion finitely-generated Z_Module is divisible
thus not the non trivial torsion finitely-generated Z_Module is divisible by LmFGND4; :: thesis: verum