theorem :: XXREAL_2:68

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