theorem Th28: :: NUMBER15:28
for n being Nat holds card { (3 |^ m) where m is Nat : ( m is odd & m <= (2 * n) + 1 ) } = n + 1