theorem RL5Th29: :: ZMODUL05:2

for V being free finite-rank Z_Module
for W being Submodule of V holds rank W <= rank V