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