let F be Field; :: thesis: for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
PencilSpace V,k is with_non_trivial_blocks
let V be finite-dimensional VectSp of F; :: thesis: for k being Nat st 1 <= k & k < dim V holds
PencilSpace V,k is with_non_trivial_blocks
let k be Nat; :: thesis: ( 1 <= k & k < dim V implies PencilSpace V,k is with_non_trivial_blocks )
assume A1: ( 1 <= k & k < dim V ) ; :: thesis: PencilSpace V,k is with_non_trivial_blocks
set S = PencilSpace V,k;
thus PencilSpace V,k is with_non_trivial_blocks :: thesis: verum

proof

let X be Block of (PencilSpace V,k); :: according to PENCIL_1:def 6 :: thesis: 2 c= card X
not PencilSpace V,k is void by A1, Th19;
then consider W1, W2 being Subspace of V such that
A2: ( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil W1,W2,k ) by Def4;
not X is trivial by A1, A2, Th17;
hence 2 c= card X by PENCIL_1:4; :: thesis: verum

end;