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