theorem Th2: :: NEWTON02:104

for n, k being Nat holds
( k + 1 in Seg n iff k < n )