theorem Th8: :: RUSUB_4:8

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