let x be Real; right_closed_halfline x is open Subset of Sorgenfrey-line
reconsider V = right_closed_halfline x as Subset of Sorgenfrey-line by Def2;
now for p being Point of Sorgenfrey-line st p in V holds
ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )let p be
Point of
Sorgenfrey-line;
( 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;
a + 0 < a + 1
by XREAL_1:6;
then consider q being
Rational such that A1:
a < q
and
q < a + 1
by RAT_1:7;
a in [.a,q.]
by A1, XXREAL_1:1;
then A2:
{a} c= [.a,q.]
by ZFMISC_1:31;
reconsider U =
[.a,q.[ as
Subset of
Sorgenfrey-line by Def2;
assume
p in V
;
ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )then
a >= x
by XXREAL_1:236;
then A3:
[.a,q.] c= V
by XXREAL_1:251;
take U =
U;
( U in BB & p in U & U c= V )thus
U in BB
by A1, Lm5;
( p in U & U c= V )thus
p in U
by A1, XXREAL_1:3;
U c= VA4:
].a,q.[ c= [.a,q.]
by XXREAL_1:37;
U = {a} \/ ].a,q.[
by A1, XXREAL_1:131;
then
U c= [.a,q.]
by A2, A4, XBOOLE_1:8;
hence
U c= V
by A3;
verum end;
hence
right_closed_halfline x is open Subset of Sorgenfrey-line
by Lm6, YELLOW_9:31; verum