theorem Th69: :: XXREAL_2:69

for A being ext-real-membered set holds A c= [.(inf A),(sup A).]