let n, m, k be Nat; :: thesis: ( k in seq (n,m) iff ( n < k & k <= n + m ) )
thus ( k in seq (n,m) implies ( n < k & k <= n + m ) ) :: thesis: ( n < k & k <= n + m implies k in seq (n,m) )

proof

assume A1: k in seq (n,m) ; :: thesis: ( n < k & k <= n + m )
then 1 + n <= k by CALCUL_2:1;
hence ( n < k & k <= n + m ) by A1, CALCUL_2:1, NAT_1:13; :: thesis: verum

end;

assume A2: ( n < k & k <= n + m ) ; :: thesis: k in seq (n,m)
then n + 1 <= k by NAT_1:13;
hence k in seq (n,m) by A2, CALCUL_2:1; :: thesis: verum