let a be Real; :: thesis: upper_bound (left_open_halfline a) = a
set X = left_open_halfline a;
A1: for s being Real st 0 < s holds
ex r being Real st
( r in left_open_halfline a & a - s < r )
proof
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in left_open_halfline a & a - s < r ) )
assume 0 < s ; :: thesis: ex r being Real 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 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