let a be real number ; :: thesis: upper_bound (left_open_halfline a) = a
set X = left_open_halfline a;
A1: for s being real number st 0 < s holds
ex r being real number st
( r in left_open_halfline a & a - s < r )

proof

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in left_open_halfline a & a - s < r ) )
assume 0 < s ; :: thesis: ex r being real number st
( r in left_open_halfline a & a - s < r )
then A2: a - s < a - 0 by XREAL_1:15;
take ((a - s) + a) / 2 ; :: thesis: ( ((a - s) + a) / 2 in left_open_halfline a & a - s < ((a - s) + a) / 2 )
((a - s) + a) / 2 < a by A2, XREAL_1:226;
hence ( ((a - s) + a) / 2 in left_open_halfline a & a - s < ((a - s) + a) / 2 ) by A2, XREAL_1:226, XXREAL_1:233; :: thesis: verum

end;

for r being real number st r in left_open_halfline a holds
r <= a by XXREAL_1:233;
hence upper_bound (left_open_halfline a) = a by A1, SEQ_4:def 1; :: thesis: verum