let V be finite-dimensional RealUnitarySpace; :: 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 ;

A is linearly-independent by RUSUB_3:def 2;

then reconsider B = A as linearly-independent Subset of V by RUSUB_3:22;

reconsider A9 = B as finite Subset of V by Th3;

reconsider V9 = V as RealUnitarySpace ;

set I = the Basis of V9;

A1: Lin the Basis of V9 = UNITSTR(# the carrier of V9, the ZeroF of V9, the addF of V9, the Mult of V9, the scalar of V9 #) by RUSUB_3:def 2;

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

A2: dim V = card I by Def2;

card A9 <= card I by A1, Th2;

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

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 ;

A is linearly-independent by RUSUB_3:def 2;

then reconsider B = A as linearly-independent Subset of V by RUSUB_3:22;

reconsider A9 = B as finite Subset of V by Th3;

reconsider V9 = V as RealUnitarySpace ;

set I = the Basis of V9;

A1: Lin the Basis of V9 = UNITSTR(# the carrier of V9, the ZeroF of V9, the addF of V9, the Mult of V9, the scalar of V9 #) by RUSUB_3:def 2;

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

A2: dim V = card I by Def2;

card A9 <= card I by A1, Th2;

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