:: deftheorem Def3 defines Subspaces_of RLVECT_5:def 3 :
for V being finite-dimensional RealLinearSpace
for n being Element of NAT
for b₃ being set holds
( b₃ = n Subspaces_of V iff for x being object holds
( x in b₃ iff ex W being strict Subspace of V st
( W = x & dim W = n ) ) );