let N, M, K be ExtNat; :: thesis: ( N <= M implies N <= M + K )
assume A1: N <= M ; :: thesis: N <= M + K
N + 0 <= M + K by A1, XXREAL_3:36;
hence N <= M + K by XXREAL_3:4; :: thesis: verum