theorem Th27: :: PENCIL_4:27

for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m & m < n & n <= dim V holds
GrassmannSpace (V,m,n) is with_non_trivial_blocks