let i, l be Nat; :: thesis: ( not i in Seg (l + 1) or i in Seg l or i = l + 1 )
A1: i is Element of NAT by ORDINAL1:def 13;
assume i in Seg (l + 1) ; :: thesis: ( i in Seg l or i = l + 1 )
then ( 1 <= i & i <= l + 1 ) by FINSEQ_1:3;
then ( ( 1 <= i & i <= l ) or i = l + 1 ) by NAT_1:8;
hence ( i in Seg l or i = l + 1 ) by A1; :: thesis: verum