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) )

set a = sup S;

set b = sup (SUP F);

assume A1: S = union F ; :: thesis: sup S = sup (SUP F)

then sup S is UpperBound of SUP F by Th4;

then A2: sup (SUP F) <= sup S by XXREAL_2:def 3;

sup (SUP F) is UpperBound of S by A1, Th5;

then sup S <= sup (SUP F) by XXREAL_2:def 3;

hence sup S = sup (SUP F) by A2, XXREAL_0:1; :: thesis: verum

sup S = sup (SUP F)

let S be non empty ext-real-membered set ; :: thesis: ( S = union F implies sup S = sup (SUP F) )

set a = sup S;

set b = sup (SUP F);

assume A1: S = union F ; :: thesis: sup S = sup (SUP F)

then sup S is UpperBound of SUP F by Th4;

then A2: sup (SUP F) <= sup S by XXREAL_2:def 3;

sup (SUP F) is UpperBound of S by A1, Th5;

then sup S <= sup (SUP F) by XXREAL_2:def 3;

hence sup S = sup (SUP F) by A2, XXREAL_0:1; :: thesis: verum