let a, b be natural Number ; :: thesis: a -' b <= a
a - b <= a - 0 by XREAL_1:230;
hence a -' b <= a by XREAL_0:def 2; :: thesis: verum