let a be real number ; :: thesis: upper_bound (left_open_halfline a) = a
set X = left_open_halfline a;
A1: for r being real number st r in left_open_halfline a holds
r <= a by XXREAL_1:233;
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 a - s < a - 0 by XREAL_1:17;
then A2: ( a - s < ((a - s) + a) / 2 & ((a - s) + a) / 2 < a ) by XREAL_1:228;
take ((a - s) + a) / 2 ; :: thesis: ( ((a - s) + a) / 2 in left_open_halfline a & a - s < ((a - s) + a) / 2 )
thus ( ((a - s) + a) / 2 in left_open_halfline a & a - s < ((a - s) + a) / 2 ) by A2, XXREAL_1:233; :: thesis: verum

end;

hence upper_bound (left_open_halfline a) = a by A1, SEQ_4:def 4; :: thesis: verum