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