let a, b be real number ; :: thesis: REAL \ (RAT a,b) = (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[

per cases ( a < b or b <= a ) ;

suppose a < b ; :: thesis: REAL \ (RAT a,b) = (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[

thus REAL \ (RAT a,b) c= (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ :: according to XBOOLE_0:def 10 :: thesis: (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ c= REAL \ (RAT a,b)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL \ (RAT a,b) or x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ )
assume A1: x in REAL \ (RAT a,b) ; :: thesis: x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[
then A2: not x in RAT a,b by XBOOLE_0:def 5;
reconsider x = x as real number by A1;

per cases ( ( x <= a & x < b ) or ( x <= a & x >= b ) or ( x > a & x < b ) or ( x > a & x >= b ) ) ;

suppose ( x <= a & x < b ) ; :: thesis: x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[

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

end;

suppose ( x <= a & x >= b ) ; :: thesis: x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[

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

end;

suppose A3: ( x > a & x < b ) ; :: thesis: x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[

x in IRRAT a,b

proof

per cases ( not x is irrational or x is irrational ) ;

suppose not x is irrational ; :: thesis: x in IRRAT a,b

hence x in IRRAT a,b by A2, A3, Th52; :: thesis: verum

end;

suppose x is irrational ; :: thesis: x in IRRAT a,b

hence x in IRRAT a,b by A3, Th53; :: thesis: verum

end;

end;

end;

then x in ].-infty ,a.] \/ (IRRAT a,b) by XBOOLE_0:def 3;
hence x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( x > a & x >= b ) ; :: thesis: x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[

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

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ or x in REAL \ (RAT a,b) )
assume A4: x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ ; :: thesis: x in REAL \ (RAT a,b)
then reconsider x = x as real number ;
A5: ( x in ].-infty ,a.] \/ (IRRAT a,b) or x in [.b,+infty .[ ) by A4, XBOOLE_0:def 3;

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

suppose x in ].-infty ,a.] ; :: thesis: x in REAL \ (RAT a,b)

then x <= a by XXREAL_1:234;
then A6: not x in RAT a,b by Th52;
x in REAL by XREAL_0:def 1;
hence x in REAL \ (RAT a,b) by A6, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A7: x in IRRAT a,b ; :: thesis: x in REAL \ (RAT a,b)

IRRAT a,b misses RAT a,b by Th84;
then A8: not x in RAT a,b by A7, XBOOLE_0:3;
x in REAL by XREAL_0:def 1;
hence x in REAL \ (RAT a,b) by A8, XBOOLE_0:def 5; :: thesis: verum

end;

suppose x in [.b,+infty .[ ; :: thesis: x in REAL \ (RAT a,b)

then x >= b by XXREAL_1:236;
then A9: not x in RAT a,b by Th52;
x in REAL by XREAL_0:def 1;
hence x in REAL \ (RAT a,b) by A9, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

suppose A10: b <= a ; :: thesis: REAL \ (RAT a,b) = (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[

then A11: ].-infty ,a.] \/ [.b,+infty .[ = REAL by Lm8;
REAL \ (RAT a,b) = REAL \ {} by A10, Lm7
.= (].-infty ,a.] \/ [.b,+infty .[) \/ (IRRAT a,b) by A11, XBOOLE_1:12
.= (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ by XBOOLE_1:4 ;
hence REAL \ (RAT a,b) = (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ ; :: thesis: verum

end;

end;