:: deftheorem Def1 defines segment PENCIL_4:def 1 :
for F being Field
for V being VectSp of F
for W1, W2 being Subspace of V
for b₅ being Subset of (Subspaces V) holds
( ( W1 is Subspace of W2 implies ( b₅ = segment (W1,W2) iff for W being strict Subspace of V holds
( W in b₅ iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) ) & ( W1 is not Subspace of W2 implies ( b₅ = segment (W1,W2) iff b₅ = {} ) ) );