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

proof

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

end;

thus not right_open_halfline a is bounded_above by Lm3; :: thesis: right_open_halfline a is connected
let r be real number ; :: according to JCT_MISC:def 1 :: thesis: for b₁ being set holds
( not r in right_open_halfline a or not b₁ in right_open_halfline a or [.r,b₁.] c= right_open_halfline a )
let s be real number ; :: thesis: ( not r in right_open_halfline a or not s in right_open_halfline a or [.r,s.] c= right_open_halfline a )
assume r in right_open_halfline a ; :: thesis: ( not s in right_open_halfline a or [.r,s.] c= right_open_halfline a )
then A7: a < r by XXREAL_1:235;
assume s in right_open_halfline a ; :: thesis: [.r,s.] c= right_open_halfline a
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [.r,s.] or x in right_open_halfline a )
assume A8: x in [.r,s.] ; :: thesis: x in right_open_halfline a
then reconsider x = x as Real ;
r <= x by A8, XXREAL_1:1;
then a < x by A7, XXREAL_0:2;
hence x in right_open_halfline a by XXREAL_1:235; :: thesis: verum