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
reconsider V' = V as RealUnitarySpace ;
consider I being Basis of V';
A1: Lin I = UNITSTR(# the carrier of V',the U2 of V',the addF of V',the Mult of V',the scalar of V' #) by RUSUB_3:def 2;
reconsider I = I as finite Subset of V by Th3;
A2: dim V = card I by Def3;
consider A being Basis of W;
reconsider A = A 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 A' = B as finite Subset of V by Th3;
card A' <= card I by A1, Th2;
hence dim W <= dim V by A2, Def3; :: thesis: verum