for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF holds
( n <= dim V iff ex W being strict Subspace of V st dim W = n ) by Lm2, Th25;