let i, l be natural Number ; :: thesis: ( not i in Seg (l + 1) or i in Seg l or i = l + 1 )
A0: i is Nat by TARSKI: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 ( ( 1 <= i & i <= l ) or i = l + 1 ) by A1, FINSEQ_1:1, NAT_1:8;
hence ( i in Seg l or i = l + 1 ) by A0; :: thesis: verum