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

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

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

sup A is UpperBound of A
by Def3;
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;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

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