theorem :: XXREAL_2:79

for A being ext-real-membered non left_end non right_end interval set ex r, s being ExtReal st
( r <= s & A = ].r,s.[ )