let n be Element of NAT ; :: thesis: for V being finite-dimensional RealLinearSpace st n <= dim V holds
ex W being strict Subspace of V st dim W = n
let V be finite-dimensional RealLinearSpace; :: 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, RLVECT_3:def 3;
then dim W = n by A2, Th29, RLVECT_3:5;
hence ex W being strict Subspace of V st dim W = n ; :: thesis: verum