let x be real number ; :: thesis: right_open_halfline x is open Subset of Sorgenfrey-line
reconsider V = right_open_halfline x as Subset of Sorgenfrey-line by Def2;
now let p be
Point of
Sorgenfrey-line ;
:: thesis: ( p in V implies ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V ) )reconsider a =
p as
Element of
REAL by Def2;
assume A1:
p in V
;
:: thesis: ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )then A2:
a > x
by XXREAL_1:235;
a + 0 < a + 1
by XREAL_1:8;
then consider q being
rational number such that A3:
(
a < q &
q < a + 1 )
by RAT_1:22;
reconsider U =
[.a,q.[ as
Subset of
Sorgenfrey-line by Def2;
take U =
U;
:: thesis: ( U in BB & p in U & U c= V )
(
q is
Element of
REAL &
x is
Element of
REAL )
by XREAL_0:def 1;
hence
U in BB
by A3, Lm5;
:: thesis: ( p in U & U c= V )thus
p in U
by A3, XXREAL_1:3;
:: thesis: U c= V
(
U = {a} \/ ].a,q.[ &
{a} c= V &
].a,q.[ c= V )
by A1, A2, A3, XXREAL_1:131, XXREAL_1:247, ZFMISC_1:37;
hence
U c= V
by XBOOLE_1:8;
:: thesis: verum end;
hence
right_open_halfline x is open Subset of Sorgenfrey-line
by Lm6, YELLOW_9:31; :: thesis: verum