for i, n being Nat st i > 1 & i in Seg n holds
i -' 1 in Seg n