theorem Th57: :: BORSUK_5:58

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