:: deftheorem Def6 defines SubspaceSet PENCIL_4:def 6 :
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat
for b₅ being Subset-Family of (m Subspaces_of V) holds
( b₅ = SubspaceSet (V,m,n) iff for X being set holds
( X in b₅ iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) );