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 V' = V as RealLinearSpace ;
consider I being Basis of V';
A1: Lin I = RLSStruct(# the carrier of V',the U2 of V',the U5 of V',the Mult of V' #) by RLVECT_3:def 3;
reconsider I = I as finite Subset of V by Th24;
consider A being Basis of W;
reconsider A = A as Subset of W ;
A2: A is linearly-independent by RLVECT_3:def 3;
then A3: A is linearly-independent Subset of V by Th15;
reconsider A' = A as finite Subset of V by A2, Th15, Th24;
A4: dim W = card A by Def3;
card A' <= card I by A1, A3, Th23;
hence dim W <= dim V by A4, Def3; :: thesis: verum