set A = left_open_halfline a;
thus
not left_open_halfline a is bounded_below
by Lm1; ( left_open_halfline a is bounded_above & left_open_halfline a is interval )
thus
left_open_halfline a is bounded_above
left_open_halfline a is interval
let r, s be ExtReal; XXREAL_2:def 12 ( not r in left_open_halfline a or not s in left_open_halfline a or [.r,s.] c= left_open_halfline a )
assume A4:
r in left_open_halfline a
; ( not s in left_open_halfline a or [.r,s.] c= left_open_halfline a )
assume A5:
s in left_open_halfline a
; [.r,s.] c= left_open_halfline a
then A6:
s < a
by XXREAL_1:233;
reconsider rr = r, ss = s as Real by A4, A5;
let x be object ; TARSKI:def 3 ( not x in [.r,s.] or x in left_open_halfline a )
assume A7:
x in [.r,s.]
; x in left_open_halfline a
then
x in [.rr,ss.]
;
then reconsider x = x as Real ;
x <= s
by A7, XXREAL_1:1;
then
x < a
by A6, XXREAL_0:2;
hence
x in left_open_halfline a
by XXREAL_1:233; verum