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