let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not SubspaceSet V,m,n is empty
let V be finite-dimensional VectSp of F; :: thesis: for m, n being Nat st n <= dim V holds
not SubspaceSet V,m,n is empty
let m, n be Nat; :: thesis: ( n <= dim V implies not SubspaceSet V,m,n is empty )
assume n <= dim V ; :: thesis: not SubspaceSet V,m,n is empty
then consider W being strict Subspace of V such that
A1: dim W = n by VECTSP_9:39;
m Subspaces_of W in SubspaceSet V,m,n by A1, Def6;
hence not SubspaceSet V,m,n is empty ; :: thesis: verum