let a be Real; :: thesis: lower_bound (right_closed_halfline a) = a
set X = right_closed_halfline a;
A1: for s being Real st 0 < s holds
ex r being Real st
( r in right_closed_halfline a & r < a + s )
proof
let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in right_closed_halfline a & r < a + s ) )
assume 0 < s ; :: thesis: ex r being Real st
( r in right_closed_halfline a & r < a + s )
then A2: a + 0 < a + s by XREAL_1:6;
take a ; :: thesis: ( a in right_closed_halfline a & a < a + s )
thus a in right_closed_halfline a by XXREAL_1:236; :: thesis: a < a + s
thus a < a + s by A2; :: thesis: verum
end;
for r being Real st r in right_closed_halfline a holds
a <= r by XXREAL_1:236;
hence lower_bound (right_closed_halfline a) = a by A1, SEQ_4:def 2; :: thesis: verum