let x be Real; left_open_halfline x is open Subset of Sorgenfrey-line
reconsider V = left_open_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;
assume A1:
p in V
;
ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )then A2:
{a} c= V
by ZFMISC_1:31;
a < x
by A1, XXREAL_1:233;
then consider q being
Rational such that A3:
a < q
and A4:
q < x
by RAT_1:7;
reconsider U =
[.a,q.[ as
Subset of
Sorgenfrey-line by Def2;
take U =
U;
( U in BB & p in U & U c= V )thus
U in BB
by A3, Lm5;
( p in U & U c= V )thus
p in U
by A3, XXREAL_1:3;
U c= VA5:
].a,q.[ c= V
by A4, XXREAL_1:263;
U = {a} \/ ].a,q.[
by A3, XXREAL_1:131;
hence
U c= V
by A2, A5, XBOOLE_1:8;
verum end;
hence
left_open_halfline x is open Subset of Sorgenfrey-line
by Lm6, YELLOW_9:31; verum