:: deftheorem Def1 defines finite-dimensional RLVECT_5:def 1 :
for V being RealLinearSpace holds
( V is finite-dimensional iff ex A being finite Subset of V st A is Basis of V );