theorem Th25: :: VECTSP_9:25

for GF being Field
for V being finite-dimensional VectSp of GF
for W being Subspace of V holds dim W <= dim V