:: deftheorem Def12 defines less_eq_dom MESFUNC1:def 11 :
for f being ext-real-valued Function
for a being ExtReal
for b₃ being set holds
( b₃ = less_eq_dom (f,a) iff for x being object holds
( x in b₃ iff ( x in dom f & f . x <= a ) ) );