theorem Thn0V: :: ZMODUL04:24

for R being Ring
for V being LeftMod of R
for W being strict Subspace of V st W <> (0). V holds
ex v being Vector of V st
( v in W & v <> 0. V )