theorem LMCLUS1: :: ZMODUL07:43

ex V being Z_Module ex p being Element of INT.Ring st
( p <> 0. INT.Ring & not VectQuot (V,(p (*) V)) is trivial )