set A = left_open_halfline a;
thus not left_open_halfline a is bounded_below by Lm1; :: thesis: ( left_open_halfline a is bounded_above & left_open_halfline a is connected )
thus left_open_halfline a is bounded_above :: thesis: left_open_halfline a is connected

proof

take a ; :: according to SEQ_4:def 1 :: thesis: for b₁ being set holds
( not b₁ in left_open_halfline a or b₁ <= a )
thus for b₁ being set holds
( not b₁ in left_open_halfline a or b₁ <= a ) by XXREAL_1:233; :: thesis: verum

end;

let r be real number ; :: according to JCT_MISC:def 1 :: thesis: for b₁ being set holds
( not r in left_open_halfline a or not b₁ in left_open_halfline a or [.r,b₁.] c= left_open_halfline a )
let s be real number ; :: thesis: ( not r in left_open_halfline a or not s in left_open_halfline a or [.r,s.] c= left_open_halfline a )
assume r in left_open_halfline a ; :: thesis: ( not s in left_open_halfline a or [.r,s.] c= left_open_halfline a )
assume s in left_open_halfline a ; :: thesis: [.r,s.] c= left_open_halfline a
then A3: s < a by XXREAL_1:233;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [.r,s.] or x in left_open_halfline a )
assume A4: x in [.r,s.] ; :: thesis: x in left_open_halfline a
then reconsider x = x as Real ;
x <= s by A4, XXREAL_1:1;
then x < a by A3, XXREAL_0:2;
hence x in left_open_halfline a by XXREAL_1:233; :: thesis: verum