theorem Th27: :: BORSUK_7:37
for r being Real
for S being Subset of R^1 st S = RAT holds
RAT /\ ].r,+infty.[ is open Subset of (R^1 | S)