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)

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))

hence
great_eq_dom (f,er) misses less_dom (f,er)
by XBOOLE_0:def 1; :: thesis: verumlet 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;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