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 st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (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 st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

let A be Element of S; :: thesis: for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

let f be PartFunc of X,REAL; :: thesis: for a being Real st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

let a be Real; :: thesis: ( A c= dom f implies A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) )

assume A4: A c= dom f ; :: thesis: A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

hence A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) by A3, XBOOLE_0:def 10; :: thesis: verum

for A being Element of S

for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (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 st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

let A be Element of S; :: thesis: for f being PartFunc of X,REAL

for a being Real st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

let f be PartFunc of X,REAL; :: thesis: for a being Real st A c= dom f holds

A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

let a be Real; :: thesis: ( A c= dom f implies A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) )

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

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

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

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

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

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

then ex y being Real st

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

then for y1 being Real holds

( not y1 = f . x or not y1 <= a ) ;

then not x in less_eq_dom (f,a) by MESFUNC6:4;

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

x in A by A1, XBOOLE_0:def 4;

hence x in A \ (A /\ (less_eq_dom (f,a))) by A2, XBOOLE_0:def 5; :: thesis: verum

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

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

then ex y being Real st

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

then for y1 being Real holds

( not y1 = f . x or not y1 <= a ) ;

then not x in less_eq_dom (f,a) by MESFUNC6:4;

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

x in A by A1, XBOOLE_0:def 4;

hence x in A \ (A /\ (less_eq_dom (f,a))) by A2, XBOOLE_0:def 5; :: thesis: verum

assume A4: A c= dom f ; :: thesis: A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))

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

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

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

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

assume A5: x in A \ (A /\ (less_eq_dom (f,a))) ; :: thesis: x in A /\ (great_dom (f,a))

then A6: x in A by XBOOLE_0:def 5;

not x in A /\ (less_eq_dom (f,a)) by A5, XBOOLE_0:def 5;

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

then not f . x <= a by A4, A6, MESFUNC6:4;

then x in great_dom (f,a) by A4, A6, MESFUNC6:5;

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

end;assume A5: x in A \ (A /\ (less_eq_dom (f,a))) ; :: thesis: x in A /\ (great_dom (f,a))

then A6: x in A by XBOOLE_0:def 5;

not x in A /\ (less_eq_dom (f,a)) by A5, XBOOLE_0:def 5;

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

then not f . x <= a by A4, A6, MESFUNC6:4;

then x in great_dom (f,a) by A4, A6, MESFUNC6:5;

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

hence A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) by A3, XBOOLE_0:def 10; :: thesis: verum