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, Th17;
then ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) by Def4;
then not X is trivial by Th16;
hence 2 c= card X by PENCIL_1:4; :: thesis: verum
end;