theorem :: XXREAL_2:76

for A being ext-real-membered non left_end right_end interval set holds A = ].(inf A),(max A).]