theorem Th24: :: VECTSP_9:24

for GF being Field
for V being VectSp of GF
for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional