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