set A = left_closed_halfline a;
not left_open_halfline a is bounded_below by Lm1;
hence not left_closed_halfline a is bounded_below by XXREAL_1:21, XXREAL_2:44; :: thesis: ( left_closed_halfline a is bounded_above & left_closed_halfline a is interval )
thus left_closed_halfline a is bounded_above ; :: thesis: left_closed_halfline a is interval
let r, s be ExtReal; :: according to XXREAL_2:def 12 :: thesis: ( not r in left_closed_halfline a or not s in left_closed_halfline a or [.r,s.] c= left_closed_halfline a )
assume A1: ( r in left_closed_halfline a & s in left_closed_halfline a ) ; :: thesis: [.r,s.] c= left_closed_halfline a
then reconsider rr = r, ss = s as Real ;
A2: s <= a by A1, XXREAL_1:234;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [.r,s.] or x in left_closed_halfline a )
assume A3: x in [.r,s.] ; :: thesis: x in left_closed_halfline a
then x in [.rr,ss.] ;
then reconsider x = x as Real ;
x <= s by A3, XXREAL_1:1;
then x <= a by A2, XXREAL_0:2;
hence x in left_closed_halfline a by XXREAL_1:234; :: thesis: verum