let V be finite-dimensional RealLinearSpace; :: thesis: for W being Subspace of V holds dim W <= dim V

let W be Subspace of V; :: thesis: dim W <= dim V

reconsider V9 = V as RealLinearSpace ;

set I = the Basis of V9;

reconsider I = the Basis of V9 as finite Subset of V by Th23;

set A = the Basis of W;

reconsider A = the Basis of W as Subset of W ;

A is linearly-independent by RLVECT_3:def 3;

then reconsider A9 = A as finite Subset of V by Th14, Th23;

( Lin I = RLSStruct(# the carrier of V9, the ZeroF of V9, the U5 of V9, the Mult of V9 #) & A is linearly-independent Subset of V ) by Th14, RLVECT_3:def 3;

then A1: card A9 <= card I by Th22;

dim W = card A by Def2;

hence dim W <= dim V by A1, Def2; :: thesis: verum

let W be Subspace of V; :: thesis: dim W <= dim V

reconsider V9 = V as RealLinearSpace ;

set I = the Basis of V9;

reconsider I = the Basis of V9 as finite Subset of V by Th23;

set A = the Basis of W;

reconsider A = the Basis of W as Subset of W ;

A is linearly-independent by RLVECT_3:def 3;

then reconsider A9 = A as finite Subset of V by Th14, Th23;

( Lin I = RLSStruct(# the carrier of V9, the ZeroF of V9, the U5 of V9, the Mult of V9 #) & A is linearly-independent Subset of V ) by Th14, RLVECT_3:def 3;

then A1: card A9 <= card I by Th22;

dim W = card A by Def2;

hence dim W <= dim V by A1, Def2; :: thesis: verum