let a, b, x be Real; :: thesis: ( a <= b implies ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ )
assume a <= b ; :: thesis: ].(x - a),(x + a).[ c= ].(x - b),(x + b).[
then ( x - b <= x - a & x + a <= x + b ) by XREAL_1:7, XREAL_1:10;
hence ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ by XXREAL_1:46; :: thesis: verum