let X be set ; :: thesis: for f being PartFunc of X,ExtREAL
for A being set
for a being R_eal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let f be PartFunc of X,ExtREAL; :: thesis: for A being set
for a being R_eal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let A be set ; :: thesis: for a being R_eal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let a be R_eal; :: thesis: A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
for x being set st x in A /\ (eq_dom (f,a)) holds
x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))

proof

let x be set ; :: thesis: ( x in A /\ (eq_dom (f,a)) implies x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) )
assume A1: x in A /\ (eq_dom (f,a)) ; :: thesis: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
then A2: x in A by XBOOLE_0:def 4;
A3: x in eq_dom (f,a) by A1, XBOOLE_0:def 4;
then A4: a = f . x by Def16;
reconsider x = x as Element of X by A1;
A5: x in dom f by A3, Def16;
then x in great_eq_dom (f,a) by A4, Def15;
then A6: x in A /\ (great_eq_dom (f,a)) by A2, XBOOLE_0:def 4;
x in less_eq_dom (f,a) by A4, A5, Def13;
hence x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

then A7: A /\ (eq_dom (f,a)) c= (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by TARSKI:def 3;
for x being set st x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) holds
x in A /\ (eq_dom (f,a))

proof

let x be set ; :: thesis: ( x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) implies x in A /\ (eq_dom (f,a)) )
assume A8: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) ; :: thesis: x in A /\ (eq_dom (f,a))
then A9: x in A /\ (great_eq_dom (f,a)) by XBOOLE_0:def 4;
A10: x in less_eq_dom (f,a) by A8, XBOOLE_0:def 4;
A11: x in A by A9, XBOOLE_0:def 4;
x in great_eq_dom (f,a) by A9, XBOOLE_0:def 4;
then A12: a <= f . x by Def15;
A13: f . x <= a by A10, Def13;
reconsider x = x as Element of X by A8;
A14: x in dom f by A10, Def13;
a = f . x by A12, A13, XXREAL_0:1;
then x in eq_dom (f,a) by A14, Def16;
hence x in A /\ (eq_dom (f,a)) by A11, XBOOLE_0:def 4; :: thesis: verum

end;

then (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) c= A /\ (eq_dom (f,a)) by TARSKI:def 3;
hence A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A7, XBOOLE_0:def 10; :: thesis: verum