for a, b being Real holds REAL \ (RAT (a,b)) = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[