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