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:35;
m Subspaces_of W in SubspaceSet (V,m,n) by A1, Def6;
hence not SubspaceSet (V,m,n) is empty ; :: thesis: verum