theorem Th40: :: XXREAL_2:40

for X being ext-real-membered set holds
( not X is empty iff inf X <= sup X )