:: deftheorem defines PencilSpace PENCIL_4:def 5 :
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat holds PencilSpace (V,k) = TopStruct(# (k Subspaces_of V),(k Pencils_of V) #);