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

proof

let x be ext-real number ; :: thesis: ( x in SUP F implies x <= sup S )
assume x in SUP F ; :: thesis: x <= sup S
then consider A being non empty ext-real-membered set such that
A2: A in F and
A3: x = sup A by Def19;
A c= S

proof

let a be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( not a in A or a in S )
assume a in A ; :: thesis: a in S
hence a in S by A1, A2, TARSKI:def 4; :: thesis: verum

end;

hence x <= sup S by A3, XXREAL_2:59; :: thesis: verum

end;

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