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