let X, Y be ext-real-membered set ; :: thesis: sup (X \/ Y) = max (sup X),(sup Y)
set a = sup (X \/ Y);
A1: sup Y is UpperBound of Y by Def3;
sup X is UpperBound of X by Def3;
then max (sup X),(sup Y) is UpperBound of X \/ Y by A1, Th65;
then A2: sup (X \/ Y) <= max (sup X),(sup Y) by Def3;
A3: sup Y <= sup (X \/ Y) by Th59, XBOOLE_1:7;
sup X <= sup (X \/ Y) by Th59, XBOOLE_1:7;
then max (sup X),(sup Y) <= sup (X \/ Y) by A3, XXREAL_0:28;
hence sup (X \/ Y) = max (sup X),(sup Y) by A2, XXREAL_0:1; :: thesis: verum