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