:: deftheorem defines <= NUMBER08:def 4 :
for f being real-valued Function
for r being Real holds
( f <= r iff for x being object st x in dom f holds
f . x <= r );