let a be Real; :: thesis: upper_bound (left_closed_halfline a) = a
set X = left_closed_halfline a;
A1: for s being Real st 0 < s holds
ex r being Real st
( r in left_closed_halfline a & a - s < r )
proof
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in left_closed_halfline a & a - s < r ) )
assume 0 < s ; :: thesis: ex r being Real st
( r in left_closed_halfline a & a - s < r )
then A2: a - s < a - 0 by XREAL_1:15;
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
thus a - s < a by A2; :: thesis: verum
end;
for r being Real st r in left_closed_halfline a holds
r <= a by XXREAL_1:234;
hence upper_bound (left_closed_halfline a) = a by A1, SEQ_4:def 1; :: thesis: verum