theorem :: VECTSP_9:36

for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF st n <= dim V holds
not n Subspaces_of V is empty