let X be non empty set ; :: thesis: for S being SigmaField of X
for A being Element of S
for f being PartFunc of X, REAL
for a being Real holds A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
let S be SigmaField of X; :: thesis: for A being Element of S
for f being PartFunc of X, REAL
for a being Real holds A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
let A be Element of S; :: thesis: for f being PartFunc of X, REAL
for a being Real holds A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
let f be PartFunc of X, REAL ; :: thesis: for a being Real holds A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
let a be Real; :: thesis: A /\ (eq_dom f,a) = (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)

now

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 x in A /\ (eq_dom f,a) ; :: thesis: x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a)
then A3: ( x in A & x in eq_dom f,a ) by XBOOLE_0:def 4;
then A4: ex y being Real st
( y = f . x & a = y ) by MESFUNC6:7;
A5: x in dom f by A3, MESFUNC6:7;
then x in great_eq_dom f,a by A4, MESFUNC6:6;
then A6: x in A /\ (great_eq_dom f,a) by A3, XBOOLE_0:def 4;
x in less_eq_dom f,a by A4, A5, MESFUNC6:4;
hence x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

then A1: A /\ (eq_dom f,a) c= (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) by TARSKI:def 3;

now

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 x in (A /\ (great_eq_dom f,a)) /\ (less_eq_dom f,a) ; :: thesis: x in A /\ (eq_dom f,a)
then A8: ( x in A /\ (great_eq_dom f,a) & x in less_eq_dom f,a ) by XBOOLE_0:def 4;
then A9: ( x in A & x in great_eq_dom f,a ) by XBOOLE_0:def 4;
then A10: ex y1 being Real st
( y1 = f . x & a <= y1 ) by MESFUNC6:6;
A11: ex y2 being Real st
( y2 = f . x & y2 <= a ) by A8, MESFUNC6:4;
A12: x in dom f by A8, MESFUNC6:4;
a = f . x by A10, A11, XXREAL_0:1;
then x in eq_dom f,a by A12, MESFUNC6:7;
hence x in A /\ (eq_dom f,a) by A9, 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 A1, XBOOLE_0:def 10; :: thesis: verum