:: deftheorem Def5 defines without-infty MESFUNC5:def 5 :
for X being non empty set
for f being PartFunc of X,ExtREAL holds
( f is without-infty iff for x being object holds -infty < f . x );