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