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 ExtReal st x in SUP F holds

x <= sup S

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 ExtReal st x in SUP F holds

x <= sup S

proof

hence
sup S is UpperBound of SUP F
by XXREAL_2:def 1; :: thesis: verum
let x be ExtReal; :: 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 Def3;

A c= S by A1, A2, TARSKI:def 4;

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

end;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 Def3;

A c= S by A1, A2, TARSKI:def 4;

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