let V be non trivial torsion finitely-generated Z_Module; :: thesis: not V is divisible
consider i being Element of INT.Ring such that
A1: ( i <> 0 & ( for v being Vector of V holds i * v = 0. V ) ) by LmTM1;
thus not V is divisible by A1, LmFGND41; :: thesis: verum