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;
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;