let a, b, r be real number ; :: thesis: ( r >= 0 & a + r <= b implies a <= b )
assume A1: ( r >= 0 & a + r <= b ) ; :: thesis: a <= b
then (a + r) - r <= b - r by XREAL_1:11;
then ( a <= b - r & b - r <= b ) by A1, XREAL_1:45;
hence a <= b by XXREAL_0:2; :: thesis: verum