theorem :: RLVECT_5:41

for n being Element of NAT
for V being finite-dimensional RealLinearSpace
for W being Subspace of V holds n Subspaces_of W c= n Subspaces_of V