theorem :: MOD_3:7

for R being Ring
for V being LeftMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} ) by VECTSP_7:10;