theorem HM8: :: ZMODUL06:47
for R being Ring
for Y being LeftMod of R
for A being Subset of Y holds Lin A is strict Subspace of (Omega). Y