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

now

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 number st
( r in R & (upper_bound R) - ((upper_bound R) - r0) < r ) by A2, Def4;
hence contradiction by A1; :: thesis: verum

end;

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