:: deftheorem Def2 defines dim RLVECT_5:def 2 :
for V being RealLinearSpace st V is finite-dimensional holds
for b₂ being Element of NAT holds
( b₂ = dim V iff for I being Basis of V holds b₂ = card I );