:: deftheorem Def2 defines Subspaces_of VECTSP_9:def 2 :
for GF being Field
for V being finite-dimensional VectSp of GF
for n being 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 ) ) );