for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF st dim V < n holds
n Subspaces_of V = {}