let r, s be real number ; :: thesis: ( r < s implies upper_bound [.r,s.[ = s )
set X = [.r,s.[;
assume A1: r < s ; :: thesis: upper_bound [.r,s.[ = s
then A2: not [.r,s.[ is empty by XXREAL_1:3;
A3: for a being real number st a in [.r,s.[ holds
a <= s by XXREAL_1:3;
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.[ & s - b < a )

proof

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

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

suppose s - b <= r ; :: thesis: contradiction

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

end;

suppose A7: s - b > r ; :: thesis: contradiction

A8: s - b < s - 0 by A5, XREAL_1:17;
then s - b < (s + (s - b)) / 2 by XREAL_1:228;
then A9: r < (s + (s - b)) / 2 by A7, XXREAL_0:2;
A10: (s + (s - b)) / 2 > s - b by A8, XREAL_1:228;
(s + (s - b)) / 2 < s by A8, XREAL_1:228;
then (s + (s - b)) / 2 in [.r,s.[ by A9, XXREAL_1:3;
hence contradiction by A6, A10; :: thesis: verum

end;

end;

end;

hence upper_bound [.r,s.[ = s by A2, A3, SEQ_4:def 4; :: thesis: verum