let r, s be Real; :: thesis: ( r < s implies lower_bound ].r,s.] = r )
set X = ].r,s.];
assume A1: r < s ; :: thesis: lower_bound ].r,s.] = r
A2: for a being Real st a in ].r,s.] holds
r <= a by XXREAL_1:2;
A3: (r + s) / 2 < s by A1, XREAL_1:226;
A4: r < (r + s) / 2 by A1, XREAL_1:226;
A5: for b being Real st 0 < b holds
ex a being Real st
( a in ].r,s.] & a < r + b )
proof
let b be Real; :: thesis: ( 0 < b implies ex a being Real st
( a in ].r,s.] & a < r + b ) )
assume that
A6: 0 < b and
A7: for a being Real st a in ].r,s.] holds
a >= r + b ; :: thesis: contradiction
per cases ( r + b > s or r + b <= s ) ;
suppose r + b > s ; :: thesis: contradiction
then A8: (r + s) / 2 < r + b by A3, XXREAL_0:2;
(r + s) / 2 in ].r,s.] by A4, A3, XXREAL_1:2;
hence contradiction by A7, A8; :: thesis: verum
end;
suppose A9: r + b <= s ; :: thesis: contradiction
A10: r < r + b by A6, XREAL_1:29;
then (r + (r + b)) / 2 < r + b by XREAL_1:226;
then A11: (r + (r + b)) / 2 < s by A9, XXREAL_0:2;
r < (r + (r + b)) / 2 by A10, XREAL_1:226;
then (r + (r + b)) / 2 in ].r,s.] by A11, XXREAL_1:2;
hence contradiction by A7, A10, XREAL_1:226; :: thesis: verum
end;
end;
end;
not ].r,s.] is empty by A1, XXREAL_1:2;
hence lower_bound ].r,s.] = r by A2, A5, SEQ_4:def 2; :: thesis: verum