:: deftheorem Def2 defines dim RUSUB_4:def 2 :
for V being RealUnitarySpace 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 );