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

proof

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

per cases ( y <= b or y > b ) ;

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

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

end;

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

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

end;

end;

end;

thus ].-infty ,a.] \/ [.b,+infty .[ c= REAL ; :: thesis: verum