let x be real number ; :: thesis: right_closed_halfline x is open Subset of Sorgenfrey-line
reconsider V = right_closed_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
p in V
;
:: thesis: ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )then A1:
a >= x
by XXREAL_1:236;
a + 0 < a + 1
by XREAL_1:8;
then consider q being
rational number such that A2:
(
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 A2, Lm5;
:: thesis: ( p in U & U c= V )thus
p in U
by A2, XXREAL_1:3;
:: thesis: U c= V
a in [.a,q.]
by A2, XXREAL_1:1;
then A3:
(
U = {a} \/ ].a,q.[ &
{a} c= [.a,q.] &
[.a,q.] c= V &
].a,q.[ c= [.a,q.] )
by A1, A2, XXREAL_1:37, XXREAL_1:131, XXREAL_1:251, ZFMISC_1:37;
then
U c= [.a,q.]
by XBOOLE_1:8;
hence
U c= V
by A3, XBOOLE_1:1;
:: thesis: verum end;
hence
right_closed_halfline x is open Subset of Sorgenfrey-line
by Lm6, YELLOW_9:31; :: thesis: verum