:: deftheorem defines pencil PENCIL_4:def 2 :
for F being Field
for V being VectSp of F
for W1, W2 being Subspace of V holds pencil (W1,W2) = (segment (W1,W2)) \ {((Omega). W1),((Omega). W2)};