theorem Th27: :: RLVECT_5:27

for V being RealLinearSpace
for W being Subspace of V st V is finite-dimensional holds
W is finite-dimensional