let V be free finite-rank Z_Module; :: thesis: for W being Submodule of V holds rank W <= rank V
let W be Submodule of V; :: thesis: rank W <= rank V
consider I being finite Subset of V such that
A1: I is Basis of V by ZMODUL03:def 3;
W is finite-rank ;
then consider A being finite Subset of W such that
A2: A is Basis of W ;
reconsider AA = A as linearly-independent Subset of V by A2, ZMODUL03:15, VECTSP_7:def 3;
card AA c= card I by A1, ZMODUL04:20;
then ( card A c< card I or card A = card I ) ;
then ( card (card A) < card (card I) or card A = card I ) by CARD_2:48;
then card A <= rank V by A1, ZMODUL03:def 5;
hence rank W <= rank V by A2, ZMODUL03:def 5; :: thesis: verum