let n, i, j, l be Nat; :: thesis: ( l in (Seg n) \ {i} & i = j + 1 & not ( 1 <= l & l <= j ) implies ( i + 1 <= l & l <= n ) )
assume that
A1: l in (Seg n) \ {i} and
A2: i = j + 1 ; :: thesis: ( ( 1 <= l & l <= j ) or ( i + 1 <= l & l <= n ) )
A3: i + 1 = j + 2 by A2;
( l in Seg n & l <> i ) by A1, ZFMISC_1:56;
hence ( ( 1 <= l & l <= j ) or ( i + 1 <= l & l <= n ) ) by A2, A3, Th4, FINSEQ_1:1; :: thesis: verum