theorem Th1: :: CHORD:1

for n being non zero Nat holds
( n - 1 is Nat & 1 <= n )