let a, b be Real; REAL \ (RAT (a,b)) = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
thus
REAL \ (RAT (a,b)) c= (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[
XBOOLE_0:def 10 (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ c= REAL \ (RAT (a,b))
let x be object ; TARSKI:def 3 ( 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.[
; 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;