for V being finite-dimensional RealUnitarySpace
for W being Subspace of V
for n being Element of NAT holds
( n <= dim V iff ex W being strict Subspace of V st dim W = n ) by Lm2, Th8;