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