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