:: deftheorem defines [. XXREAL_1:def 2 :
for r, s being ExtReal holds [.r,s.[ = { a where a is Element of ExtREAL : ( r <= a & a < s ) } ;