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