let n, k be Nat; :: thesis: ( k in Segm (n + 1) implies n - k is Nat )
assume A1: k in Segm (n + 1) ; :: thesis: n - k is Nat
n + 1 > k by A1, NAT_1:44;
then n >= k by NAT_1:13;
then n - k >= k - k by XREAL_1:9;
hence n - k is Nat by INT_1:3; :: thesis: verum