theorem Thn0V: :: ZMODUL04:24

for V being Z_Module
for W being strict Submodule of V st W <> (0). V holds
ex v being Vector of V st
( v in W & v <> 0. V )