let x be Real; :: thesis: right_closed_halfline x is open Subset of Sorgenfrey-line

reconsider V = right_closed_halfline x as Subset of Sorgenfrey-line by Def2;

reconsider V = right_closed_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 )

hence
right_closed_halfline x is open Subset of Sorgenfrey-line
by Lm6, YELLOW_9:31; :: thesis: verumex 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;

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 ; :: thesis: 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; :: thesis: ( U in BB & p in U & U c= V )

thus U in BB by A1, Lm5; :: thesis: ( p in U & U c= V )

thus p in U by A1, XXREAL_1:3; :: thesis: U c= V

A4: ].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; :: thesis: verum

end;( 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 ; :: thesis: 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; :: thesis: ( U in BB & p in U & U c= V )

thus U in BB by A1, Lm5; :: thesis: ( p in U & U c= V )

thus p in U by A1, XXREAL_1:3; :: thesis: U c= V

A4: ].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; :: thesis: verum