theorem :: PENCIL_4:29

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