let n be Element of NAT ; :: thesis: for V being finite-dimensional RealLinearSpace st n <= dim V holds
not n Subspaces_of V is empty
let V be finite-dimensional RealLinearSpace; :: thesis: ( n <= dim V implies not n Subspaces_of V is empty )
assume n <= dim V ; :: thesis: not n Subspaces_of V is empty
then consider W being strict Subspace of V such that
A1: dim W = n by Lm2;
thus not n Subspaces_of V is empty by A1, Def4; :: thesis: verum