theorem Th0: :: AFINSQ_1:1

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