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