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 A1: 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 A2: x in REAL \ (RAT a,b) ; :: thesis: x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[
then A3: ( x in REAL & not x in RAT a,b ) by XBOOLE_0:def 5;
reconsider x = x as real number by A2;

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 A4: ( 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 A1, A3, A4, Th52; :: thesis: verum

end;

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

hence x in IRRAT a,b by A1, A4, 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 A5: x in (].-infty ,a.] \/ (IRRAT a,b)) \/ [.b,+infty .[ ; :: thesis: x in REAL \ (RAT a,b)
then reconsider x = x as real number ;
A6: ( x in ].-infty ,a.] \/ (IRRAT a,b) or x in [.b,+infty .[ ) by A5, XBOOLE_0:def 3;

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

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

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

end;

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

A8: x in REAL by XREAL_0:def 1;
IRRAT a,b misses RAT a,b by A1, Th84;
then not x in RAT a,b by A7, XBOOLE_0:3;
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 ( x in REAL & not x in RAT a,b ) by A1, Th52, XREAL_0:def 1;
hence x in REAL \ (RAT a,b) by XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

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

then A10: ].-infty ,a.] \/ [.b,+infty .[ = REAL by Lm11;
REAL \ (RAT a,b) = REAL \ {} by A9, Lm10
.= (].-infty ,a.] \/ [.b,+infty .[) \/ (IRRAT a,b) by A10, 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;