let a be Real; :: thesis: lower_bound (right_open_halfline a) = a
set X = right_open_halfline a;
A1: for s being Real st 0 < s holds
ex r being Real st
( r in right_open_halfline a & r < a + s )

proof

let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in right_open_halfline a & r < a + s ) )
assume 0 < s ; :: thesis: ex r being Real st
( r in right_open_halfline a & r < a + s )
then A2: a + 0 < a + s by XREAL_1:6;
take ((a + a) + s) / 2 ; :: thesis: ( ((a + a) + s) / 2 in right_open_halfline a & ((a + a) + s) / 2 < a + s )
a < (a + (a + s)) / 2 by A2, XREAL_1:226;
hence ( ((a + a) + s) / 2 in right_open_halfline a & ((a + a) + s) / 2 < a + s ) by A2, XREAL_1:226, XXREAL_1:235; :: thesis: verum

end;

for r being Real st r in right_open_halfline a holds
a <= r by XXREAL_1:235;
hence lower_bound (right_open_halfline a) = a by A1, SEQ_4:def 2; :: thesis: verum