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