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_eq_dom (f,a)) = A \ (A /\ (less_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_eq_dom (f,a)) = A \ (A /\ (less_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_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
let f be PartFunc of X,REAL; :: thesis: for a being Real st A c= dom f holds
A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
let a be Real; :: thesis: ( A c= dom f implies A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) )
now :: thesis: for x being object st x in A /\ (great_eq_dom (f,a)) holds
x in A \ (A /\ (less_dom (f,a)))
let x be object ; :: thesis: ( x in A /\ (great_eq_dom (f,a)) implies x in A \ (A /\ (less_dom (f,a))) )
assume A1: x in A /\ (great_eq_dom (f,a)) ; :: thesis: x in A \ (A /\ (less_dom (f,a)))
then x in great_eq_dom (f,a) by XBOOLE_0:def 4;
then ex y being Real st
( y = f . x & a <= y ) by MESFUNC6:6;
then for y1 being Real holds
( not y1 = f . x or not y1 < a ) ;
then not x in less_dom (f,a) by MESFUNC6:3;
then A2: not x in A /\ (less_dom (f,a)) by XBOOLE_0:def 4;
x in A by A1, XBOOLE_0:def 4;
hence x in A \ (A /\ (less_dom (f,a))) by A2, XBOOLE_0:def 5; :: thesis: verum
end;
then A3: A /\ (great_eq_dom (f,a)) c= A \ (A /\ (less_dom (f,a))) by TARSKI:def 3;
assume A4: A c= dom f ; :: thesis: A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
now :: thesis: for x being object st x in A \ (A /\ (less_dom (f,a))) holds
x in A /\ (great_eq_dom (f,a))
let x be object ; :: thesis: ( x in A \ (A /\ (less_dom (f,a))) implies x in A /\ (great_eq_dom (f,a)) )
assume A5: x in A \ (A /\ (less_dom (f,a))) ; :: thesis: x in A /\ (great_eq_dom (f,a))
then A6: x in A by XBOOLE_0:def 5;
not x in A /\ (less_dom (f,a)) by A5, XBOOLE_0:def 5;
then not x in less_dom (f,a) by A6, XBOOLE_0:def 4;
then not f . x < a by A4, A6, MESFUNC6:3;
then x in great_eq_dom (f,a) by A4, A6, MESFUNC6:6;
hence x in A /\ (great_eq_dom (f,a)) by A6, XBOOLE_0:def 4; :: thesis: verum
end;
then A \ (A /\ (less_dom (f,a))) c= A /\ (great_eq_dom (f,a)) by TARSKI:def 3;
hence A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) by A3, XBOOLE_0:def 10; :: thesis: verum