let x, y be real number ; :: thesis: [.x,y.[ is open Subset of Sorgenfrey-line
reconsider V = [.x,y.[ as Subset of Sorgenfrey-line by Def2;

now

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;
A1: x is Element of REAL by XREAL_0:def 1;
assume A2: p in [.x,y.[ ; :: thesis: ex U being Subset of Sorgenfrey-line st
( U in BB & p in U & U c= V )
then A3: x <= a by XXREAL_1:3;
a < y by A2, XXREAL_1:3;
then consider q being rational number such that
A4: a < q and
A5: 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 )
A6: q is Element of REAL by XREAL_0:def 1;
x < q by A3, A4, XXREAL_0:2;
hence U in BB by A1, A6, Lm5; :: thesis: ( p in U & U c= V )
thus p in U by A3, A4, XXREAL_1:3; :: thesis: U c= V
thus U c= V by A5, XXREAL_1:38; :: thesis: verum

end;

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