theorem :: XXREAL_2:62

for X being ext-real-membered set
for x being ExtReal st ex y being ExtReal st
( y in X & y <= x ) holds
inf X <= x