:: deftheorem defines without+infty MESFUNC5:def 4 :
for R being Relation holds
( R is without+infty iff not +infty in rng R );