theorem :: ZMODUL05:8

for V being free finite-rank Z_Module
for n being Nat st n <= rank V holds
not n Submodules_of V is empty