let l, n, i, j be Element of NAT ; :: thesis: ( l in (Seg n) \ {i} & i = j + 1 & not ( 1 <= l & l <= j ) implies ( i + 1 <= l & l <= n ) )
assume A1: ( l in (Seg n) \ {i} & i = j + 1 ) ; :: thesis: ( ( 1 <= l & l <= j ) or ( i + 1 <= l & l <= n ) )
then A2: ( l in Seg n & l <> i ) by ZFMISC_1:64;
i + 1 = j + 2 by A1;
hence ( ( 1 <= l & l <= j ) or ( i + 1 <= l & l <= n ) ) by A1, A2, Th4, FINSEQ_1:3; :: thesis: verum