let F be Field; :: thesis: 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
let V be finite-dimensional VectSp of F; :: thesis: for k being Nat st 1 <= k & k < dim V holds
not PencilSpace (V,k) is void
let k be Nat; :: thesis: ( 1 <= k & k < dim V implies not PencilSpace (V,k) is void )
assume A1: ( 1 <= k & k < dim V ) ; :: thesis: not PencilSpace (V,k) is void
set S = PencilSpace (V,k);
not the topology of (PencilSpace (V,k)) is empty by A1, Th11;
hence not PencilSpace (V,k) is void by PENCIL_1:def 4; :: thesis: verum