let A, B be ext-real-membered set ; :: thesis: sup (A \/ B) = max (sup A),(sup B)
set m = max (sup A),(sup B);
B: sup A is UpperBound of A by Def3;
sup B is UpperBound of B by Def3;
then A: max (sup A),(sup B) is UpperBound of A \/ B by B, Th5B;
for x being UpperBound of A \/ B holds max (sup A),(sup B) <= x

proof

let x be UpperBound of A \/ B; :: thesis: max (sup A),(sup B) <= x
x is UpperBound of A by Th4B, XBOOLE_1:7;
then C: sup A <= x by Def3;
x is UpperBound of B by Th4B, XBOOLE_1:7;
then sup B <= x by Def3;
hence max (sup A),(sup B) <= x by C, XXREAL_0:28; :: thesis: verum

end;

hence sup (A \/ B) = max (sup A),(sup B) by A, Def3; :: thesis: verum