:: deftheorem defines halfline PROB_1:def 10 :
for r being ExtReal holds halfline r = ].-infty,r.[;