theorem Th2: :: CHORD:2

for n being odd Nat holds
( n - 1 is Nat & 1 <= n ) by Th1;