let n, i be Nat; :: thesis: ( i is Nat of n iff i in Seg (n + 1) )
( i is Nat of n iff ( 1 <= i & i <= n + 1 ) ) by Def2;
hence ( i is Nat of n iff i in Seg (n + 1) ) by FINSEQ_1:1; :: thesis: verum