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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in REAL \ (RAT (a,b)) ; :: thesis:
then A2: not x in RAT (a,b) by XBOOLE_0:def 5;
reconsider x = x as Real by A1;

per cases ;

suppose ( x <= a & x < b ) ; :: thesis:

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:

end;

suppose ( x <= a & x >= b ) ; :: thesis:

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:

end;

suppose A3: ( x > a & x < b ) ; :: thesis:

x in IRRAT (a,b)

proof

per cases ;

suppose x is rational ; :: thesis:

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

end;

suppose x is irrational ; :: thesis:

hence x in IRRAT (a,b) by A3, Th29; :: thesis:

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:

end;

suppose ( x > a & x >= b ) ; :: thesis:

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:

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A4: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ ; :: thesis:
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 by A5, XBOOLE_0:def 3;

suppose x in ].-infty,a.] ; :: thesis:

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:

end;

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

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:

end;

suppose x in [.b,+infty.[ ; :: thesis:

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:

end;

end;