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