theorem Th9: :: HILB10_7:9

for m being Nat st m <> 0 holds
2 * (card (bool ((Seg m) \ {1}))) = card (bool ((Seg (1 + m)) \ {1}))