let R be non empty Subset of REAL; :: thesis: for r0 being Real st ( for r being Real st r in R holds
r <= r0 ) holds
upper_bound R <= r0
let r0 be Real; :: thesis: ( ( for r being Real st r in R holds
r <= r0 ) implies upper_bound R <= r0 )
assume A1: for r being Real st r in R holds
r <= r0 ; :: thesis: upper_bound R <= r0
then for r being ExtReal st r in R holds
r <= r0 ;
then r0 is UpperBound of R by XXREAL_2:def 1;
then A2: R is bounded_above ;

now :: thesis: not upper_bound R > r0

set r1 = (upper_bound R) - r0;
assume upper_bound R > r0 ; :: thesis: contradiction
then (upper_bound R) - r0 > 0 by XREAL_1:50;
then ex r being Real st
( r in R & (upper_bound R) - ((upper_bound R) - r0) < r ) by A2, Def1;
hence contradiction by A1; :: thesis: verum

end;

hence upper_bound R <= r0 ; :: thesis: verum