:: deftheorem Def12 defines interval XXREAL_2:def 12 :
for A being ext-real-membered set holds
( A is interval iff for r, s being ExtReal st r in A & s in A holds
[.r,s.] c= A );