theorem Th28: :: RLVECT_5:28

for V being finite-dimensional RealLinearSpace
for W being Subspace of V holds dim W <= dim V