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

proof

let s be real number ; :: thesis: ( 0 < s implies ex r being real number st
( r in left_closed_halfline a & a - s < r ) )
assume A2: 0 < s ; :: thesis: ex r being real number st
( r in left_closed_halfline a & a - s < r )
take a ; :: thesis: ( a in left_closed_halfline a & a - s < a )
thus a in left_closed_halfline a by XXREAL_1:234; :: thesis: a - s < a
a - s < a - 0 by A2, XREAL_1:17;
hence a - s < a ; :: thesis: verum

end;

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