theorem :: RLVECT_5:39

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