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

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