let x be Real; :: 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 :: thesis: 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; :: 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} c= V by ZFMISC_1:31;
a + 0 < a + 1 by XREAL_1:6;
then consider q being Rational such that
A3: a < q and
q < a + 1 by RAT_1:7;
reconsider U = [.a,q.[ as Subset of Sorgenfrey-line by Def2;
take U = U; :: thesis: ( U in BB & p in U & U c= V )
thus 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
a > x by A1, XXREAL_1:235;
then A4: ].a,q.[ c= V by XXREAL_1:247;
U = {a} \/ ].a,q.[ by A3, XXREAL_1:131;
hence U c= V by A2, A4, XBOOLE_1:8; :: thesis: verum

end;

hence right_open_halfline x is open Subset of Sorgenfrey-line by Lm6, YELLOW_9:31; :: thesis: verum