let a, b, c be Real; :: thesis: ( a <= c & c <= b implies ].-infty,c.] \/ [.a,b.] = ].-infty,b.] )
assume that
A1: a <= c and
A2: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in ].-infty,c.] \/ [.a,b.] or x in ].-infty,b.] )
assume A3: x in ].-infty,c.] \/ [.a,b.] ; :: thesis: x in ].-infty,b.]
then reconsider x = x as Real ;

per cases ( x in ].-infty,c.] or x in [.a,b.] ) by A3, 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 A2, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in ].-infty,b.] or x in ].-infty,c.] \/ [.a,b.] )
assume A4: x in ].-infty,b.] ; :: thesis: x in ].-infty,c.] \/ [.a,b.]
then reconsider x = x as Real ;

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 A5: x > c ; :: thesis: x in ].-infty,c.] \/ [.a,b.]

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

end;

end;