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:3;
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:3;
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:3;
hence contradiction by A7, A10, XREAL_1:226; :: thesis: verum

end;

end;

end;

not [.r,s.[ is empty by A1, XXREAL_1:3;
hence lower_bound [.r,s.[ = r by A2, A5, SEQ_4:def 2; :: thesis: verum