let a, b be Real; :: 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 object ; :: 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 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 ( x is rational or x is irrational ) ;

suppose x is rational ; :: thesis: x in IRRAT (a,b)

hence x in IRRAT (a,b) by A2, A3, Th28; :: thesis: verum

end;

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

hence x in IRRAT (a,b) by A3, Th29; :: 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 object ; :: 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 ;
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 Th28;
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 Th56;
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 Th28;
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;