let a, b, r be Real; :: thesis: ( r >= 0 & a + r <= b implies a <= b )
assume ( r >= 0 & a + r <= b ) ; :: thesis: a <= b
then ( (a + r) - r <= b - r & b - r <= b ) by XREAL_1:9, XREAL_1:43;
hence a <= b by XXREAL_0:2; :: thesis: verum