:: deftheorem defines left_closed_halfline LIMFUNC1:def 1 :
for r being Real holds left_closed_halfline r = ].-infty,r.];