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