let n, k be Nat; :: thesis: ( k + 1 in Seg n iff k < n )
thus ( k + 1 in Seg n implies k < n ) :: thesis: ( k < n implies k + 1 in Seg n )

proof

assume k + 1 in Seg n ; :: thesis: k < n
then k + 1 <= n by FINSEQ_1:1;
hence k < n by NAT_1:13; :: thesis: verum

end;

thus ( k < n implies k + 1 in Seg n ) by FINSEQ_3:11; :: thesis: verum