let X, Y be ext-real-membered set ; :: thesis: sup (X /\ Y) <= min (sup X),(sup Y)
A1: sup Y is UpperBound of Y by Def3;
sup X is UpperBound of X by Def3;
then min (sup X),(sup Y) is UpperBound of X /\ Y by A1, Th69;
hence sup (X /\ Y) <= min (sup X),(sup Y) by Def3; :: thesis: verum