let F be bool_DOMAIN of ExtREAL ; :: thesis: for S being non empty ext-real-membered set st S = union F holds
sup S = sup (SUP F)
let S be non empty ext-real-membered set ; :: thesis: ( S = union F implies sup S = sup (SUP F) )
assume A1: S = union F ; :: thesis: sup S = sup (SUP F)
set a = sup S;
set b = sup (SUP F);
A2: sup (SUP F) is UpperBound of S by A1, Th113;
sup S is UpperBound of SUP F by A1, Th112;
then ( sup S <= sup (SUP F) & sup (SUP F) <= sup S ) by A2, XXREAL_2:def 3;
hence sup S = sup (SUP F) by XXREAL_0:1; :: thesis: verum