let i, l be Nat; :: thesis: ( not i in Seg (l + 1) or i in Seg l or i = l + 1 )
assume A1: i in Seg (l + 1) ; :: thesis: ( i in Seg l or i = l + 1 )
then i <= l + 1 by FINSEQ_1:1;
then A2: ( ( 1 <= i & i <= l ) or i = l + 1 ) by A1, FINSEQ_1:1, NAT_1:8;
thus ( i in Seg l or i = l + 1 ) by A2; :: thesis: verum