theorem :: RLVECT_5:40

for n being Element of NAT
for V being finite-dimensional RealLinearSpace st dim V < n holds
n Subspaces_of V = {}