let n, m, k be Nat; :: thesis: ( k < m implies n + k in n + m )
assume m > k ; :: thesis: n + k in n + m
then k + n < n + m by XREAL_1:8;
then n + k in Segm (n + m) by NAT_1:44;
hence n + k in n + m ; :: thesis: verum