for n, i, j, l being Nat st l in (Seg n) \ {i} & i = j + 1 & not ( 1 <= l & l <= j ) holds
( i + 1 <= l & l <= n )