let x, a, b be Real; :: thesis: ( a <= b implies ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ )
assume A1: a <= b ; :: thesis: ].(x - a),(x + a).[ c= ].(x - b),(x + b).[

now :: thesis: for r being Real st r in ].(x - a),(x + a).[ holds
r in ].(x - b),(x + b).[

let r be Real; :: thesis: ( r in ].(x - a),(x + a).[ implies r in ].(x - b),(x + b).[ )
assume r in ].(x - a),(x + a).[ ; :: thesis: r in ].(x - b),(x + b).[
then A2: ( x - a < r & r < x + a ) by XXREAL_1:4;
x - b <= x - a by A1, XREAL_1:13;
then A3: x - b < r by A2, XXREAL_0:2;
x + a <= x + b by A1, XREAL_1:7;
then r < x + b by A2, XXREAL_0:2;
hence r in ].(x - b),(x + b).[ by A3; :: thesis: verum

end;

hence ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ ; :: thesis: verum