let a, b, c be real number ; :: thesis: ( a <= c & c <= b implies ].-infty ,c.] \/ [.a,b.] = ].-infty ,b.] )
assume A1: ( a <= c & c <= b ) ; :: thesis: ].-infty ,c.] \/ [.a,b.] = ].-infty ,b.]
thus ].-infty ,c.] \/ [.a,b.] c= ].-infty ,b.] :: according to XBOOLE_0:def 10 :: thesis: ].-infty ,b.] c= ].-infty ,c.] \/ [.a,b.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ].-infty ,c.] \/ [.a,b.] or x in ].-infty ,b.] )
assume A2: x in ].-infty ,c.] \/ [.a,b.] ; :: thesis: x in ].-infty ,b.]
then reconsider x = x as real number ;

per cases ( x in ].-infty ,c.] or x in [.a,b.] ) by A2, XBOOLE_0:def 3;

suppose x in ].-infty ,c.] ; :: thesis: x in ].-infty ,b.]

then x <= c by XXREAL_1:234;
then x <= b by A1, XXREAL_0:2;
hence x in ].-infty ,b.] by XXREAL_1:234; :: thesis: verum

end;

suppose x in [.a,b.] ; :: thesis: x in ].-infty ,b.]

then x <= b by XXREAL_1:1;
hence x in ].-infty ,b.] by XXREAL_1:234; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ].-infty ,b.] or x in ].-infty ,c.] \/ [.a,b.] )
assume A3: x in ].-infty ,b.] ; :: thesis: x in ].-infty ,c.] \/ [.a,b.]
then reconsider x = x as real number ;

per cases ( x <= c or x > c ) ;

suppose x <= c ; :: thesis: x in ].-infty ,c.] \/ [.a,b.]

then x in ].-infty ,c.] by XXREAL_1:234;
hence x in ].-infty ,c.] \/ [.a,b.] by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x > c ; :: thesis: x in ].-infty ,c.] \/ [.a,b.]

then A4: x > a by A1, XXREAL_0:2;
x <= b by A3, XXREAL_1:234;
then x in [.a,b.] by A4, XXREAL_1:1;
hence x in ].-infty ,c.] \/ [.a,b.] by XBOOLE_0:def 3; :: thesis: verum

end;

end;