let A, B be ext-real-membered set ; :: thesis: sup (A \/ B) = max (sup A),(sup B)
set m = max (sup A),(sup B);
A1: sup B is UpperBound of B by Def3;
A2: 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 B by Th6, XBOOLE_1:7;
then A3: sup B <= x by Def3;
x is UpperBound of A by Th6, XBOOLE_1:7;
then sup A <= x by Def3;
hence max (sup A),(sup B) <= x by A3, XXREAL_0:28; :: thesis: verum

end;

sup A is UpperBound of A by Def3;
then max (sup A),(sup B) is UpperBound of A \/ B by A1, Th8;
hence sup (A \/ B) = max (sup A),(sup B) by A2, Def3; :: thesis: verum