let X be set ; :: thesis: for P being with_empty_element semi-diff-closed Subset-Family of X
for M being pre-Measure of P
for A, B being set st A in P & B in P & A \ B in P & B c= A holds
M . A >= M . B
let P be with_empty_element semi-diff-closed Subset-Family of X; :: thesis: for M being pre-Measure of P
for A, B being set st A in P & B in P & A \ B in P & B c= A holds
M . A >= M . B
let M be pre-Measure of P; :: thesis: for A, B being set st A in P & B in P & A \ B in P & B c= A holds
M . A >= M . B
let A, B be set ; :: thesis: ( A in P & B in P & A \ B in P & B c= A implies M . A >= M . B )
assume that
A1: ( A in P & B in P & A \ B in P ) and
A2: B c= A ; :: thesis: M . A >= M . B
consider F being disjoint_valued FinSequence of P such that
A3: A \ B = Union F by A1, SRINGS_3:def 1;
A7: rng <*B*> = {B} by FINSEQ_1:38;
then reconsider G = <*B*> as disjoint_valued FinSequence of P by FINSEQ_1:def 4, A1, ZFMISC_1:31;
now :: thesis: not union (rng G) meets union (rng F)
assume union (rng G) meets union (rng F) ; :: thesis: contradiction
then consider x being object such that
A4: ( x in union (rng G) & x in union (rng F) ) by XBOOLE_0:3;
consider P being set such that
A5: ( x in P & P in rng G ) by A4, TARSKI:def 4;
P in {B} by A5, FINSEQ_1:38;
then A6: x in B by A5, TARSKI:def 1;
x in A \ B by A3, A4, CARD_3:def 4;
hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum
end;
then reconsider H = G ^ F as disjoint_valued FinSequence of P by Th43;
A8: union (rng G) = B by A7, ZFMISC_1:25;
rng H = (rng G) \/ (rng F) by FINSEQ_1:31;
then union (rng H) = (union (rng G)) \/ (union (rng F)) by ZFMISC_1:78;
then Union H = B \/ (union (rng F)) by A8, CARD_3:def 4
.= B \/ (A \ B) by A3, CARD_3:def 4 ;
then Union H = A \/ B by XBOOLE_1:39;
then Union H = A by A2, XBOOLE_1:12;
then A9: M . A = Sum (M * H) by A1, Def8;
Union G = B by A8, CARD_3:def 4;
then A10: M . B = Sum (M * G) by A1, Def8;
B0: now :: thesis: not -infty in rng (M * G)
assume -infty in rng (M * G) ; :: thesis: contradiction
then consider n being Element of NAT such that
B1: ( n in dom (M * G) & -infty = (M * G) . n ) by PARTFUN1:3;
M . (G . n) = -infty by B1, FUNCT_1:12;
hence contradiction by SUPINF_2:51; :: thesis: verum
end;
A11: now :: thesis: not -infty in rng (M * F)
assume -infty in rng (M * F) ; :: thesis: contradiction
then consider n being Element of NAT such that
B2: ( n in dom (M * F) & -infty = (M * F) . n ) by PARTFUN1:3;
M . (F . n) = -infty by B2, FUNCT_1:12;
hence contradiction by SUPINF_2:51; :: thesis: verum
end;
A12: now :: thesis: for n being Nat st n in dom (M * F) holds
(M * F) . n >= 0
let n be Nat; :: thesis: ( n in dom (M * F) implies (M * F) . n >= 0 )
assume n in dom (M * F) ; :: thesis: (M * F) . n >= 0
then ( (M * F) . n = M . (F . n) & F . n in dom M ) by FUNCT_1:11, FUNCT_1:12;
hence (M * F) . n >= 0 by SUPINF_2:51; :: thesis: verum
end;
M * H = (M * G) ^ (M * F) by FINSEQOP:9;
then Sum (M * H) = (Sum (M * G)) + (Sum (M * F)) by A11, B0, EXTREAL1:10;
hence M . B <= M . A by A9, A10, A12, MESFUNC5:53, XXREAL_3:39; :: thesis: verum