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