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

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

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 :: thesis: for x being object st x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) holds

x in A /\ (eq_dom (f,a))

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

let x be object ; :: thesis: ( x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) implies x in A /\ (eq_dom (f,a)) )

assume A1: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) ; :: thesis: x in A /\ (eq_dom (f,a))

then A2: x in less_eq_dom (f,a) by XBOOLE_0:def 4;

then A3: x in dom f by MESFUNC6:4;

A4: x in A /\ (great_eq_dom (f,a)) by A1, XBOOLE_0:def 4;

then x in great_eq_dom (f,a) by XBOOLE_0:def 4;

then A5: ex y1 being Real st

( y1 = f . x & a <= y1 ) by MESFUNC6:6;

ex y2 being Real st

( y2 = f . x & y2 <= a ) by A2, MESFUNC6:4;

then a = f . x by A5, XXREAL_0:1;

then A6: x in eq_dom (f,a) by A3, MESFUNC6:7;

x in A by A4, XBOOLE_0:def 4;

hence x in A /\ (eq_dom (f,a)) by A6, XBOOLE_0:def 4; :: thesis: verum

end;assume A1: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) ; :: thesis: x in A /\ (eq_dom (f,a))

then A2: x in less_eq_dom (f,a) by XBOOLE_0:def 4;

then A3: x in dom f by MESFUNC6:4;

A4: x in A /\ (great_eq_dom (f,a)) by A1, XBOOLE_0:def 4;

then x in great_eq_dom (f,a) by XBOOLE_0:def 4;

then A5: ex y1 being Real st

( y1 = f . x & a <= y1 ) by MESFUNC6:6;

ex y2 being Real st

( y2 = f . x & y2 <= a ) by A2, MESFUNC6:4;

then a = f . x by A5, XXREAL_0:1;

then A6: x in eq_dom (f,a) by A3, MESFUNC6:7;

x in A by A4, XBOOLE_0:def 4;

hence x in A /\ (eq_dom (f,a)) by A6, XBOOLE_0:def 4; :: thesis: verum

now :: thesis: for x being object st x in A /\ (eq_dom (f,a)) holds

x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))

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

let x be object ; :: thesis: ( x in A /\ (eq_dom (f,a)) implies x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) )

assume A8: x in A /\ (eq_dom (f,a)) ; :: thesis: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))

then A9: x in A by XBOOLE_0:def 4;

A10: x in eq_dom (f,a) by A8, XBOOLE_0:def 4;

then A11: ex y being Real st

( y = f . x & a = y ) by MESFUNC6:7;

A12: x in dom f by A10, MESFUNC6:7;

then x in great_eq_dom (f,a) by A11, MESFUNC6:6;

then A13: x in A /\ (great_eq_dom (f,a)) by A9, XBOOLE_0:def 4;

x in less_eq_dom (f,a) by A11, A12, MESFUNC6:4;

hence x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A13, XBOOLE_0:def 4; :: thesis: verum

end;assume A8: x in A /\ (eq_dom (f,a)) ; :: thesis: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))

then A9: x in A by XBOOLE_0:def 4;

A10: x in eq_dom (f,a) by A8, XBOOLE_0:def 4;

then A11: ex y being Real st

( y = f . x & a = y ) by MESFUNC6:7;

A12: x in dom f by A10, MESFUNC6:7;

then x in great_eq_dom (f,a) by A11, MESFUNC6:6;

then A13: x in A /\ (great_eq_dom (f,a)) by A9, XBOOLE_0:def 4;

x in less_eq_dom (f,a) by A11, A12, MESFUNC6:4;

hence x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A13, XBOOLE_0:def 4; :: thesis: verum

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