let V be finite-dimensional RealUnitarySpace; :: thesis: for n being Element of NAT st n <= dim V holds
ex W being strict Subspace of V st dim W = n
let n be Element of NAT ; :: thesis: ( n <= dim V implies ex W being strict Subspace of V st dim W = n )
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
assume n <= dim V ; :: thesis: ex W being strict Subspace of V st dim W = n
then n <= card I by A1, Def2;
then consider A being finite Subset of I such that
A2: card A = n by FINSEQ_4:72;
reconsider A = A as Subset of V by XBOOLE_1:1;
reconsider W = Lin A as strict finite-dimensional Subspace of V ;
I is linearly-independent by A1, RUSUB_3:def 2;
then dim W = n by A2, Th9, RLVECT_3:5;
hence ex W being strict Subspace of V st dim W = n ; :: thesis: verum