consider V being Z_Module, p being Element of INT.Ring such that
A1: ( p <> 0. INT.Ring & not VectQuot (V,(p (*) V)) is trivial ) by LMCLUS1;
reconsider pp = p as non zero Element of INT.Ring by A1, STRUCT_0:def 12;
set W = VectQuot (V,(pp (*) V));
not VectQuot (V,(pp (*) V)) is trivial by A1;
hence not for b₁ being torsion Z_Module holds b₁ is trivial ; :: thesis: verum