:: deftheorem defines right_closed_halfline LIMFUNC1:def 2 :
for r being Real holds right_closed_halfline r = [.r,+infty.[;