let r be Real; :: thesis: for S being Subset of R^1 st S = RAT holds
RAT /\ ].-infty,r.[ is open Subset of (R^1 | S)
let S be Subset of R^1; :: thesis: ( S = RAT implies RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) )
assume A1: S = RAT ; :: thesis: RAT /\ ].-infty,r.[ is open Subset of (R^1 | S)
set X = ].-infty,r.[;
reconsider R = RAT /\ ].-infty,r.[ as Subset of (R^1 | (R^1 QQ)) by Lm8, XBOOLE_1:17;
A2: R^1 ].-infty,r.[ is open by BORSUK_5:40;
R = (R^1 ].-infty,r.[) /\ the carrier of (R^1 | (R^1 QQ)) by PRE_TOPC:8;
hence RAT /\ ].-infty,r.[ is open Subset of (R^1 | S) by A1, A2, TSP_1:def 1; :: thesis: verum