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