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, Th65;
hence sup (X /\ Y) <= min ((sup X),(sup Y)) by Def3; :: thesis: verum