theorem :: CHORD:9

for n being odd Nat holds
( not n <= 8 or n = 1 or n = 3 or n = 5 or n = 7 )