:: deftheorem defines right_open_halfline LIMFUNC1:def 3 :
for r being Real holds right_open_halfline r = ].r,+infty.[;