theorem HM8: :: ZMODUL06:47

for Y being Z_Module
for A being Subset of Y holds Lin A is strict Submodule of (Omega). Y