let F be bool_DOMAIN of ExtREAL ; :: thesis: for S being ext-real-membered set st S = union F holds
sup (SUP F) is UpperBound of S
let S be ext-real-membered set ; :: thesis: ( S = union F implies sup (SUP F) is UpperBound of S )
assume A1: S = union F ; :: thesis: sup (SUP F) is UpperBound of S
for x being ext-real number st x in S holds
x <= sup (SUP F)

proof

let x be ext-real number ; :: thesis: ( x in S implies x <= sup (SUP F) )
assume x in S ; :: thesis: x <= sup (SUP F)
then consider Z being set such that
A2: ( x in Z & Z in F ) by A1, TARSKI:def 4;
reconsider Z = Z as non empty ext-real-membered set by A2;
consider a being set such that
A3: a = sup Z ;
reconsider a = a as ext-real number by A3;
A4: sup Z is UpperBound of Z by XXREAL_2:def 3;
a in SUP F by A2, A3, Def19;
hence x <= sup (SUP F) by A3, A4, A2, XXREAL_2:61, XXREAL_2:def 1; :: thesis: verum

end;

hence sup (SUP F) is UpperBound of S by XXREAL_2:def 1; :: thesis: verum