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