:: deftheorem defines ]. RCOMP_1:def 8 :
for g being ExtReal
for s being Real holds ].g,s.] = { r where r is Real : ( g < r & r <= s ) } ;