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 ex W being strict Subspace of V st dim W = n by Lm2;

hence not n Subspaces_of V is empty by Def3; :: thesis: verum

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 ex W being strict Subspace of V st dim W = n by Lm2;

hence not n Subspaces_of V is empty by Def3; :: thesis: verum