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