theorem Th3: :: RLAFFIN3:3

for V being RealLinearSpace holds
( V is finite-dimensional iff (Omega). V is finite-dimensional )