theorem :: XXREAL_2:67

for X, Y being ext-real-membered set holds sup (X /\ Y) <= min ((sup X),(sup Y))