let r, s be Real; :: thesis: ( r < s implies upper_bound ].r,s.] = s )
set X = ].r,s.];
assume A1: r < s ; :: thesis: upper_bound ].r,s.] = s
A2: for a being Real st a in ].r,s.] holds
a <= s by XXREAL_1:2;
A3: r < (r + s) / 2 by A1, XREAL_1:226;
A4: (r + s) / 2 < s by A1, XREAL_1:226;
A5: for b being Real st 0 < b holds
ex a being Real st
( a in ].r,s.] & s - b < a )

proof

let b be Real; :: thesis: ( 0 < b implies ex a being Real st
( a in ].r,s.] & s - b < a ) )
assume that
A6: 0 < b and
A7: for a being Real st a in ].r,s.] holds
a <= s - b ; :: thesis: contradiction

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

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

then A8: (r + s) / 2 > s - b by A3, XXREAL_0:2;
(r + s) / 2 in ].r,s.] by A3, A4, XXREAL_1:2;
hence contradiction by A7, A8; :: thesis: verum

end;

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

A10: s - b < s - 0 by A6, XREAL_1:15;
then s - b < (s + (s - b)) / 2 by XREAL_1:226;
then A11: r < (s + (s - b)) / 2 by A9, XXREAL_0:2;
(s + (s - b)) / 2 < s by A10, XREAL_1:226;
then (s + (s - 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 upper_bound ].r,s.] = s by A2, A5, SEQ_4:def 1; :: thesis: verum