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 )

thus ( k + 1 in Seg n implies k < n ) :: thesis: ( k < n implies k + 1 in Seg n )

proof

thus
( k < n implies k + 1 in Seg n )
by FINSEQ_3:11; :: thesis: verum
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;then k + 1 <= n by FINSEQ_1:1;

hence k < n by NAT_1:13; :: thesis: verum