:: deftheorem Def4 defines Pencils_of PENCIL_4:def 4 :
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat
for b₄ being Subset-Family of (k Subspaces_of V) holds
( b₄ = k Pencils_of V iff for X being set holds
( X in b₄ iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) );