theorem Th4: :: LMOD_7:4

for K being Ring
for V being LeftMod of K st not V is trivial holds
for A being Subset of V st A is base holds
A <> {}