let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not GrassmannSpace V,m,n is void
let V be finite-dimensional VectSp of F; :: thesis: for m, n being Nat st n <= dim V holds
not GrassmannSpace V,m,n is void
let m, n be Nat; :: thesis: ( n <= dim V implies not GrassmannSpace V,m,n is void )
assume n <= dim V ; :: thesis: not GrassmannSpace V,m,n is void
then not the topology of (GrassmannSpace V,m,n) is empty by Th24;
hence not GrassmannSpace V,m,n is void by PENCIL_1:def 4; :: thesis: verum