theorem Th22: :: PENCIL_4:22

for F being Field
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