for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
PencilSpace (V,k) is PLS by Th17, Th18, Th19, Th20, VECTSP_9:36;