theorem Th17: :: PENCIL_4:17

for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
not PencilSpace (V,k) is void by Th10;