for n, i being Nat st i in Seg n holds
ex j, k being Nat st
( n = (j + 1) + k & i = j + 1 )