for n being Element of NAT
for V being finite-dimensional RealLinearSpace st n <= dim V holds
not n Subspaces_of V is empty