theorem :: ZMODUL08:33

for V being non trivial free Z_Module
for v being Vector of (DivisibleMod V) ex a being Element of INT.Ring st
( a in NAT & a <> 0 & a * v in EMbedding V & ( for b being Element of INT.Ring st b in NAT & b < a & b <> 0 holds
not b * v in EMbedding V ) )