for X being set
for f being PartFunc of X,ExtREAL
for er being ExtReal holds great_eq_dom (f,er) misses less_dom (f,er)