let r, s be real number ; :: thesis: ( r < s implies lower_bound ].r,s.] = r )
set X = ].r,s.];
assume A1: r < s ; :: thesis: lower_bound ].r,s.] = r
then A2: not ].r,s.] is empty by XXREAL_1:2;
A3: for a being real number st a in ].r,s.] holds
r <= a by XXREAL_1:2;
reconsider r = r, s = s as Real by XREAL_0:def 1;
A4: ( r < (r + s) / 2 & (r + s) / 2 < s ) by A1, XREAL_1:228;
for b being real number st 0 < b holds
ex a being real number st
( a in ].r,s.] & a < r + b )

proof

let b be real number ; :: thesis: ( 0 < b implies ex a being real number st
( a in ].r,s.] & a < r + b ) )
assume that
A5: 0 < b and
A6: for a being real number st a in ].r,s.] holds
a >= r + b ; :: thesis: contradiction
reconsider b = b as Real by XREAL_0:def 1;

per cases ( r + b > s or r + b <= s ) ;

suppose r + b > s ; :: thesis: contradiction

then ( (r + s) / 2 in ].r,s.] & (r + s) / 2 < r + b ) by A4, XXREAL_0:2, XXREAL_1:2;
hence contradiction by A6; :: thesis: verum

end;

suppose A7: r + b <= s ; :: thesis: contradiction

A8: r < r + b by A5, XREAL_1:31;
then A9: r < (r + (r + b)) / 2 by XREAL_1:228;
A10: (r + (r + b)) / 2 < r + b by A8, XREAL_1:228;
then (r + (r + b)) / 2 < s by A7, XXREAL_0:2;
then (r + (r + b)) / 2 in ].r,s.] by A9, XXREAL_1:2;
hence contradiction by A6, A10; :: thesis: verum

end;

end;

end;

hence lower_bound ].r,s.] = r by A2, A3, SEQ_4:def 5; :: thesis: verum