let x, y be Real; :: thesis: [.x,y.[ is open Subset of Sorgenfrey-line

reconsider V = [.x,y.[ as Subset of Sorgenfrey-line by Def2;

reconsider V = [.x,y.[ as Subset of Sorgenfrey-line by Def2;

now :: thesis: for p being Point of Sorgenfrey-line st p in [.x,y.[ holds

ex U being Subset of Sorgenfrey-line st

( U in BB & p in U & U c= V )

hence
[.x,y.[ 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 [.x,y.[ 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 [.x,y.[ ; :: thesis: ex U being Subset of Sorgenfrey-line st

( U in BB & p in U & U c= V )

then A2: x <= a by XXREAL_1:3;

a < y by A1, XXREAL_1:3;

then consider q being Rational such that

A3: a < q and

A4: q < y by RAT_1:7;

reconsider U = [.x,q.[ as Subset of Sorgenfrey-line by Def2;

take U = U; :: thesis: ( U in BB & p in U & U c= V )

x < q by A2, A3, XXREAL_0:2;

hence U in BB by Lm5; :: thesis: ( p in U & U c= V )

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

thus U c= V by A4, XXREAL_1:38; :: thesis: verum

end;( U in BB & p in U & U c= V ) )

reconsider a = p as Element of REAL by Def2;

assume A1: p in [.x,y.[ ; :: thesis: ex U being Subset of Sorgenfrey-line st

( U in BB & p in U & U c= V )

then A2: x <= a by XXREAL_1:3;

a < y by A1, XXREAL_1:3;

then consider q being Rational such that

A3: a < q and

A4: q < y by RAT_1:7;

reconsider U = [.x,q.[ as Subset of Sorgenfrey-line by Def2;

take U = U; :: thesis: ( U in BB & p in U & U c= V )

x < q by A2, A3, XXREAL_0:2;

hence U in BB by Lm5; :: thesis: ( p in U & U c= V )

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

thus U c= V by A4, XXREAL_1:38; :: thesis: verum