theorem Th4: :: POLYNOM9:4
for m being positive Nat holds card (bool ((Seg m) \ {1})) = 2 |^ (m -' 1)