let GF be Field; :: thesis: for n being Nat
for V being finite-dimensional VectSp of GF st n <= dim V holds
not n Subspaces_of V is empty
let n be Nat; :: thesis: for V being finite-dimensional VectSp of GF st n <= dim V holds
not n Subspaces_of V is empty
let V be finite-dimensional VectSp of GF; :: 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 Def2; :: thesis: verum