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:3;
then A2: ( ( 1 <= i & i <= l ) or i = l + 1 ) by A1, FINSEQ_1:3, NAT_1:8;
i is Element of NAT by ORDINAL1:def 13;
hence ( i in Seg l or i = l + 1 ) by A2; :: thesis: verum