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

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