set A = right_closed_halfline a;
thus right_closed_halfline a is bounded_below :: thesis: ( not right_closed_halfline a is bounded_above & right_closed_halfline a is interval )

proof

take a ; :: according to XXREAL_2:def 9 :: thesis: a is LowerBound of right_closed_halfline a
let x be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not x in right_closed_halfline a or a <= x )
thus ( not x in right_closed_halfline a or a <= x ) by XXREAL_1:236; :: thesis: verum

end;

not right_open_halfline a is bounded_above by Lm2;
hence not right_closed_halfline a is bounded_above by XXREAL_1:22, XXREAL_2:43; :: thesis: right_closed_halfline a is interval
let r, s be ext-real number ; :: according to XXREAL_2:def 12 :: thesis: ( not r in right_closed_halfline a or not s in right_closed_halfline a or [.r,s.] c= right_closed_halfline a )
assume Z: r in right_closed_halfline a ; :: thesis: ( not s in right_closed_halfline a or [.r,s.] c= right_closed_halfline a )
then A5: a <= r by XXREAL_1:236;
assume s in right_closed_halfline a ; :: thesis: [.r,s.] c= right_closed_halfline a
then reconsider rr = r, ss = s as Real by Z;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [.r,s.] or x in right_closed_halfline a )
assume A6: x in [.r,s.] ; :: thesis: x in right_closed_halfline a
then x in [.rr,ss.] ;
then reconsider x = x as Real ;
r <= x by A6, XXREAL_1:1;
then a <= x by A5, XXREAL_0:2;
hence x in right_closed_halfline a by XXREAL_1:236; :: thesis: verum