let X be set ; :: thesis: for f being PartFunc of X,ExtREAL
for er being ExtReal holds great_eq_dom (f,er) misses less_dom (f,er)
let f be PartFunc of X,ExtREAL; :: thesis: for er being ExtReal holds great_eq_dom (f,er) misses less_dom (f,er)
let er be ExtReal; :: thesis: great_eq_dom (f,er) misses less_dom (f,er)

now :: thesis: for x being object holds not x in (great_eq_dom (f,er)) /\ (less_dom (f,er))

let x be object ; :: thesis: not x in (great_eq_dom (f,er)) /\ (less_dom (f,er))
assume x in (great_eq_dom (f,er)) /\ (less_dom (f,er)) ; :: thesis: contradiction
then ( x in great_eq_dom (f,er) & x in less_dom (f,er) ) by XBOOLE_0:def 4;
then ( f . x >= er & f . x < er ) by MESFUNC1:def 11, MESFUNC1:def 14;
hence contradiction ; :: thesis: verum

end;

hence great_eq_dom (f,er) misses less_dom (f,er) by XBOOLE_0:def 1; :: thesis: verum