set A = right_open_halfline a;
thus
right_open_halfline a is bounded_below
( not right_open_halfline a is bounded_above & right_open_halfline a is interval )
thus
not right_open_halfline a is bounded_above
by Lm2; right_open_halfline a is interval
let r, s be ExtReal; XXREAL_2:def 12 ( not r in right_open_halfline a or not s in right_open_halfline a or [.r,s.] c= right_open_halfline a )
assume A11:
r in right_open_halfline a
; ( not s in right_open_halfline a or [.r,s.] c= right_open_halfline a )
then A12:
a < r
by XXREAL_1:235;
assume
s in right_open_halfline a
; [.r,s.] c= right_open_halfline a
then reconsider rr = r, ss = s as Real by A11;
let x be object ; TARSKI:def 3 ( not x in [.r,s.] or x in right_open_halfline a )
assume A13:
x in [.r,s.]
; x in right_open_halfline a
then
x in [.rr,ss.]
;
then reconsider x = x as Real ;
r <= x
by A13, XXREAL_1:1;
then
a < x
by A12, XXREAL_0:2;
hence
x in right_open_halfline a
by XXREAL_1:235; verum