let GF be Field; :: thesis: for V being finite-dimensional VectSp of GF
for W being Subspace of V holds dim W <= dim V
let V be finite-dimensional VectSp of GF; :: thesis: for W being Subspace of V holds dim W <= dim V
let W be Subspace of V; :: thesis: dim W <= dim V
set A = the Basis of W;
reconsider A = the Basis of W as Subset of W ;
A1: dim W = card A by Def1;
A is linearly-independent by VECTSP_7:def 3;
then reconsider B = A as linearly-independent Subset of V by Th11;
reconsider A9 = B as finite Subset of V by Th20;
reconsider V9 = V as VectSp of GF ;
set I = the Basis of V9;
A2: Lin the Basis of V9 = ModuleStr(# the carrier of V9, the U5 of V9, the ZeroF of V9, the lmult of V9 #) by VECTSP_7:def 3;
reconsider I = the Basis of V9 as finite Subset of V by Th20;
card A9 <= card I by A2, Th19;
hence dim W <= dim V by A1, Def1; :: thesis: verum