theorem :: RLVECT_5:31

for V being finite-dimensional RealLinearSpace
for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )