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