theorem :: XXREAL_2:60

for X, Y being ext-real-membered set st X c= Y holds
inf Y <= inf X