:: MEASURE3 semantic presentation

REAL is non empty V33() V59() V60() V61() V65() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty V60() set
is non empty V67() set
bool is non empty set
bool ExtREAL is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() set
bool omega is non empty set
is non empty V66() V67() V68() set
bool is non empty set
bool () is non empty set
RAT is non empty V33() V59() V60() V61() V62() V65() set
INT is non empty V33() V59() V60() V61() V62() V63() V65() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

+infty is V23() set
-infty is V23() set
X is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
Ser X is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
S is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
Ser S is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool

rng (Ser X) is non empty V47() V60() Element of bool ExtREAL
rng (Ser S) is non empty V47() V60() Element of bool ExtREAL
M is ext-real set
dom (Ser X) is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
A is set
(Ser X) . A is ext-real Element of ExtREAL

(Ser S) . B is ext-real Element of ExtREAL
B2 is ext-real Element of ExtREAL
dom (Ser S) is V59() V60() V61() V62() V63() V64() Element of bool NAT
sup (rng (Ser X)) is ext-real Element of ExtREAL
sup (rng (Ser S)) is ext-real Element of ExtREAL
X is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
Ser X is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
S is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
Ser S is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool

(Ser S) . M is ext-real Element of ExtREAL
(Ser X) . M is ext-real Element of ExtREAL

(Ser X) . M is ext-real Element of ExtREAL
(Ser S) . M is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
rng M is set
rng M is non empty Element of bool (bool X)
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
(X,S,A) is non empty V47() N_Measure_fam of S
meet (X,S,A) is Element of S
M . (meet (X,S,A)) is ext-real Element of ExtREAL
B is Element of S
M . B is ext-real Element of ExtREAL
B2 is set
C2 is set
dom A is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
C1 is set
A . C1 is set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
(X,S,M) is non empty V47() N_Measure_fam of S
union (X,S,M) is Element of S
(X,S,A) is non empty V47() N_Measure_fam of S
meet (X,S,A) is Element of S
(A . 0) \ (meet (X,S,A)) is Element of S
dom M is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
B is set
B2 is set
C2 is set
M . C2 is set

D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . O is Element of S
(A . 0) \ (A . O) is Element of S
B is set
B2 is set
B2 is set
dom A is V59() V60() V61() V62() V63() V64() Element of bool NAT
C2 is set
A . C2 is set

A . C1 is Element of S
(A . 0) \ (A . C1) is Element of S
C1 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
M . (C1 + 1) is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
(X,S,A) is non empty V47() N_Measure_fam of S
meet (X,S,A) is Element of S
(X,S,M) is non empty V47() N_Measure_fam of S
union (X,S,M) is Element of S
(A . 0) \ (union (X,S,M)) is Element of S

A . B is Element of S
B + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
A . (B + 1) is Element of S
the Element of (X,S,A) is Element of (X,S,A)
B2 is set
dom A is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
C2 is set
A . C2 is set
(A . 0) /\ (meet (X,S,A)) is Element of S
(A . 0) \ (meet (X,S,A)) is Element of S
(A . 0) \ ((A . 0) \ (meet (X,S,A))) is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B . 0 is Element of S
M . (B . 0) is ext-real Element of ExtREAL
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
(X,S,B) is non empty V47() N_Measure_fam of S
meet (X,S,B) is Element of S
M . (meet (X,S,B)) is ext-real Element of ExtREAL
(X,S,A) is non empty V47() N_Measure_fam of S
union (X,S,A) is Element of S
M . (union (X,S,A)) is ext-real Element of ExtREAL
(M . (B . 0)) - (M . (union (X,S,A))) is ext-real Element of ExtREAL
K183((M . (union (X,S,A)))) is ext-real set
K182((M . (B . 0)),K183((M . (union (X,S,A))))) is ext-real set
(B . 0) \ (meet (X,S,B)) is Element of S
(B . 0) \ (union (X,S,A)) is Element of S
M . ((B . 0) \ (union (X,S,A))) is ext-real Element of ExtREAL
M . ((B . 0) \ (meet (X,S,B))) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B . 0 is Element of S
M . (B . 0) is ext-real Element of ExtREAL
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
(X,S,A) is non empty V47() N_Measure_fam of S
union (X,S,A) is Element of S
M . (union (X,S,A)) is ext-real Element of ExtREAL
(X,S,B) is non empty V47() N_Measure_fam of S
meet (X,S,B) is Element of S
M . (meet (X,S,B)) is ext-real Element of ExtREAL
(M . (B . 0)) - (M . (meet (X,S,B))) is ext-real Element of ExtREAL
K183((M . (meet (X,S,B)))) is ext-real set
K182((M . (B . 0)),K183((M . (meet (X,S,B))))) is ext-real set
(B . 0) \ (union (X,S,A)) is Element of S
(B . 0) \ (meet (X,S,B)) is Element of S
M . ((B . 0) \ (meet (X,S,B))) is ext-real Element of ExtREAL
M . ((B . 0) \ (union (X,S,A))) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B . 0 is Element of S
M . (B . 0) is ext-real Element of ExtREAL
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
(X,S,B) is non empty V47() N_Measure_fam of S
meet (X,S,B) is Element of S
M . (meet (X,S,B)) is ext-real Element of ExtREAL
M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
rng (M * A) is non empty V47() V60() Element of bool ExtREAL
sup (rng (M * A)) is ext-real Element of ExtREAL
(M . (B . 0)) - (sup (rng (M * A))) is ext-real Element of ExtREAL
K183((sup (rng (M * A)))) is ext-real set
K182((M . (B . 0)),K183((sup (rng (M * A))))) is ext-real set

A . B2 is Element of S
B2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
A . (B2 + 1) is Element of S
(X,S,A) is non empty V47() N_Measure_fam of S
union (X,S,A) is Element of S
M . (union (X,S,A)) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B . 0 is Element of S
M . (B . 0) is ext-real Element of ExtREAL
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
M * B is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
rng (M * B) is non empty V47() V60() Element of bool ExtREAL
inf (rng (M * B)) is ext-real Element of ExtREAL
M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
rng (M * A) is non empty V47() V60() Element of bool ExtREAL
sup (rng (M * A)) is ext-real Element of ExtREAL
B2 is Element of S
M . B2 is ext-real Element of ExtREAL
C2 is ext-real set
dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
C1 is set
(M * A) . C1 is ext-real Element of ExtREAL

A . D2 is Element of S
M . (A . D2) is ext-real Element of ExtREAL

O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . B2 is Element of S
(B . 0) \ (B . B2) is Element of S
C2 is ext-real set
dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
C1 is set
(M * B) . C1 is ext-real Element of ExtREAL
(M * B) . 0 is ext-real Element of ExtREAL
dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
C2 is ext-real Element of ExtREAL
(M * A) . 0 is ext-real Element of ExtREAL
C1 is ext-real Element of ExtREAL
dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
D2 is set
(M * A) . D2 is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B . 0 is Element of S
M . (B . 0) is ext-real Element of ExtREAL
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
rng (M * A) is non empty V47() V60() Element of bool ExtREAL
sup (rng (M * A)) is ext-real Element of ExtREAL
M * B is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
rng (M * B) is non empty V47() V60() Element of bool ExtREAL
inf (rng (M * B)) is ext-real Element of ExtREAL
(M . (B . 0)) - (inf (rng (M * B))) is ext-real Element of ExtREAL
K183((inf (rng (M * B)))) is ext-real set
K182((M . (B . 0)),K183((inf (rng (M * B))))) is ext-real set
C2 is ext-real set
dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
C1 is set
(M * A) . C1 is ext-real Element of ExtREAL

A . D2 is Element of S
dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT
(B . 0) \ (A . D2) is Element of S
M . ((B . 0) \ (A . D2)) is ext-real Element of ExtREAL
(M * B) . 0 is ext-real Element of ExtREAL

B . O is Element of S
O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
B . (O + 1) is Element of S

O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . B2 is Element of S
M . (B . B2) is ext-real Element of ExtREAL
(M * B) . B2 is ext-real Element of ExtREAL
(B . 0) \ (B . B2) is Element of S
(B . 0) \ ((B . 0) \ (B . B2)) is Element of S
(B . 0) /\ (B . B2) is Element of S

O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . B2 is Element of S
(B . 0) \ (B . B2) is Element of S
M . (A . D2) is ext-real Element of ExtREAL

B2 is V22() V23() ext-real Element of REAL
D2 is V22() V23() ext-real Element of REAL
O1 is V22() V23() ext-real Element of REAL
(M . (B . 0)) - O is ext-real Element of ExtREAL
K183(O) is ext-real set
K182((M . (B . 0)),K183(O)) is ext-real set
B2 - D2 is V22() V23() ext-real Element of REAL
((M . (B . 0)) - O) + O is ext-real Element of ExtREAL
(B2 - D2) + D2 is V22() V23() ext-real Element of REAL
(inf (rng (M * B))) + O is ext-real Element of ExtREAL
O1 + D2 is V22() V23() ext-real Element of REAL
((inf (rng (M * B))) + O) - (inf (rng (M * B))) is ext-real Element of ExtREAL
K182(((inf (rng (M * B))) + O),K183((inf (rng (M * B))))) is ext-real set
D2 + O1 is V22() V23() ext-real Element of REAL
(D2 + O1) - O1 is V22() V23() ext-real Element of REAL

A . C2 is Element of S
C2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
A . (C2 + 1) is Element of S
C2 is ext-real UpperBound of rng (M * A)
(X,S,B) is non empty V47() N_Measure_fam of S
meet (X,S,B) is Element of S
M . (meet (X,S,B)) is ext-real Element of ExtREAL
C1 is ext-real set
dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
D2 is set
(M * B) . D2 is ext-real Element of ExtREAL

B . O is Element of S
M . (B . O) is ext-real Element of ExtREAL
(X,S,A) is non empty V47() N_Measure_fam of S
union (X,S,A) is Element of S
M . (union (X,S,A)) is ext-real Element of ExtREAL
(M . (B . 0)) - (M . (meet (X,S,B))) is ext-real Element of ExtREAL
K183((M . (meet (X,S,B)))) is ext-real set
K182((M . (B . 0)),K183((M . (meet (X,S,B))))) is ext-real set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B . 0 is Element of S
M . (B . 0) is ext-real Element of ExtREAL
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
M * B is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
rng (M * B) is non empty V47() V60() Element of bool ExtREAL
inf (rng (M * B)) is ext-real Element of ExtREAL
M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
rng (M * A) is non empty V47() V60() Element of bool ExtREAL
sup (rng (M * A)) is ext-real Element of ExtREAL
(M . (B . 0)) - (sup (rng (M * A))) is ext-real Element of ExtREAL
K183((sup (rng (M * A)))) is ext-real set
K182((M . (B . 0)),K183((sup (rng (M * A))))) is ext-real set
C2 is ext-real set
dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
C1 is set
(M * B) . C1 is ext-real Element of ExtREAL
D2 is ext-real Element of ExtREAL
O is V22() V23() ext-real Element of REAL
B2 is V22() V23() ext-real Element of REAL
D2 is V22() V23() ext-real Element of REAL
(sup (rng (M * A))) + D2 is ext-real Element of ExtREAL
D2 + B2 is V22() V23() ext-real Element of REAL
((sup (rng (M * A))) + D2) - (sup (rng (M * A))) is ext-real Element of ExtREAL
K182(((sup (rng (M * A))) + D2),K183((sup (rng (M * A))))) is ext-real set
B2 + D2 is V22() V23() ext-real Element of REAL
(B2 + D2) - D2 is V22() V23() ext-real Element of REAL
dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT
(M . (B . 0)) - D2 is ext-real Element of ExtREAL
K183(D2) is ext-real set
K182((M . (B . 0)),K183(D2)) is ext-real set

O1 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
c15 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
B . c15 is Element of S
c15 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
B . (c15 + 1) is Element of S
B . O1 is Element of S
M . (B . O1) is ext-real Element of ExtREAL
(M . (B . 0)) - (M . (B . O1)) is ext-real Element of ExtREAL
K183((M . (B . O1))) is ext-real set
K182((M . (B . 0)),K183((M . (B . O1)))) is ext-real set
(B . 0) \ (B . O1) is Element of S
M . ((B . 0) \ (B . O1)) is ext-real Element of ExtREAL
A . (O1 + 1) is Element of S
M . (A . (O1 + 1)) is ext-real Element of ExtREAL
(M * A) . (O1 + 1) is ext-real Element of ExtREAL
O - B2 is V22() V23() ext-real Element of REAL
((M . (B . 0)) - D2) + D2 is ext-real Element of ExtREAL
(O - B2) + B2 is V22() V23() ext-real Element of REAL
C2 is V22() V23() ext-real Element of REAL
C1 is V22() V23() ext-real Element of REAL
D2 is V22() V23() ext-real Element of REAL
(sup (rng (M * A))) + (inf (rng (M * B))) is ext-real Element of ExtREAL
C2 + D2 is V22() V23() ext-real Element of REAL
((sup (rng (M * A))) + (inf (rng (M * B)))) - (sup (rng (M * A))) is ext-real Element of ExtREAL
K182(((sup (rng (M * A))) + (inf (rng (M * B)))),K183((sup (rng (M * A))))) is ext-real set
D2 + C2 is V22() V23() ext-real Element of REAL
(D2 + C2) - C2 is V22() V23() ext-real Element of REAL
O is ext-real LowerBound of rng (M * B)
(M . (B . 0)) - (inf (rng (M * B))) is ext-real Element of ExtREAL
K183((inf (rng (M * B)))) is ext-real set
K182((M . (B . 0)),K183((inf (rng (M * B))))) is ext-real set
B2 is ext-real Element of ExtREAL
D2 is ext-real Element of ExtREAL
O1 is ext-real Element of ExtREAL
C1 - D2 is V22() V23() ext-real Element of REAL
((M . (B . 0)) - (inf (rng (M * B)))) + O1 is ext-real Element of ExtREAL
(C1 - D2) + D2 is V22() V23() ext-real Element of REAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
M . (A . 0) is ext-real Element of ExtREAL
(X,S,A) is non empty V47() N_Measure_fam of S
meet (X,S,A) is Element of S
M . (meet (X,S,A)) is ext-real Element of ExtREAL
M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
rng (M * A) is non empty V47() V60() Element of bool ExtREAL
inf (rng (M * A)) is ext-real Element of ExtREAL
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B . 0 is Element of S
(X,S,B) is non empty V47() N_Measure_fam of S
union (X,S,B) is Element of S
(A . 0) \ (meet (X,S,A)) is Element of S
(A . 0) \ (union (X,S,B)) is Element of S
M . ((A . 0) \ (union (X,S,B))) is ext-real Element of ExtREAL
B2 is Element of S
M . B2 is ext-real Element of ExtREAL
(M . (A . 0)) - (M . B2) is ext-real Element of ExtREAL
K183((M . B2)) is ext-real set
K182((M . (A . 0)),K183((M . B2))) is ext-real set
M . ((A . 0) \ (meet (X,S,A))) is ext-real Element of ExtREAL

B . B2 is Element of S
B2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
B . (B2 + 1) is Element of S
M . (union (X,S,B)) is ext-real Element of ExtREAL
M * B is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
rng (M * B) is non empty V47() V60() Element of bool ExtREAL
sup (rng (M * B)) is ext-real Element of ExtREAL
(M . (A . 0)) - (sup (rng (M * B))) is ext-real Element of ExtREAL
K183((sup (rng (M * B)))) is ext-real set
K182((M . (A . 0)),K183((sup (rng (M * B))))) is ext-real set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative V90(X,S) Element of bool
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) V53() Element of bool [:NAT,S:]
M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
SUM (M * A) is ext-real Element of ExtREAL
(X,S,A) is non empty V47() N_Measure_fam of S
union (X,S,A) is Element of S
M . (union (X,S,A)) is ext-real Element of ExtREAL
A . 0 is Element of S
B2 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B2 . 0 is Element of S
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
{(union (X,S,A)),{}} is non empty set
C2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]
rng C2 is Element of bool (bool X)
bool (bool X) is non empty set
C2 . 0 is Element of bool X
C1 is set
Ser (M * A) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set

B2 . D2 is Element of S
D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
A . (D2 + 1) is Element of S
(B2 . D2) /\ (A . (D2 + 1)) is Element of S

B2 . O is Element of S
O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
B2 . (O + 1) is Element of S

A . B2 is Element of S
(B2 . (O + 1)) /\ (A . B2) is Element of S
A . (O + 1) is Element of S
(A . (O + 1)) /\ (A . B2) is Element of S
(A . (O + 1)) \/ (B2 . O) is Element of S
((A . (O + 1)) \/ (B2 . O)) /\ (A . B2) is Element of S
(B2 . O) /\ (A . B2) is Element of S
((A . (O + 1)) /\ (A . B2)) \/ ((B2 . O) /\ (A . B2)) is Element of S

A . O is Element of S
(B2 . 0) /\ (A . O) is Element of S

(Ser (M * A)) . D2 is ext-real Element of ExtREAL
B2 . D2 is Element of S
M . (B2 . D2) is ext-real Element of ExtREAL
D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
(Ser (M * A)) . (D2 + 1) is ext-real Element of ExtREAL
B2 . (D2 + 1) is Element of S
M . (B2 . (D2 + 1)) is ext-real Element of ExtREAL
A . (D2 + 1) is Element of S
(B2 . D2) /\ (A . (D2 + 1)) is Element of S
(M * A) . (D2 + 1) is ext-real Element of ExtREAL
(M . (B2 . D2)) + ((M * A) . (D2 + 1)) is ext-real Element of ExtREAL
M . (A . (D2 + 1)) is ext-real Element of ExtREAL
(M . (B2 . D2)) + (M . (A . (D2 + 1))) is ext-real Element of ExtREAL
(A . (D2 + 1)) \/ (B2 . D2) is Element of S
M . ((A . (D2 + 1)) \/ (B2 . D2)) is ext-real Element of ExtREAL
(Ser (M * A)) . 0 is ext-real Element of ExtREAL
(M * A) . 0 is ext-real Element of ExtREAL
M . (B2 . 0) is ext-real Element of ExtREAL
C1 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
M * C1 is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
Ser (M * C1) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool

(Ser (M * C1)) . D2 is ext-real Element of ExtREAL
D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
(Ser (M * C1)) . (D2 + 1) is ext-real Element of ExtREAL
C1 . (D2 + 1) is Element of S
dom (M * C1) is V59() V60() V61() V62() V63() V64() Element of bool NAT
(M * C1) . (D2 + 1) is ext-real Element of ExtREAL

(M . (union (X,S,A))) + ((M * C1) . (D2 + 1)) is ext-real Element of ExtREAL
(Ser (M * C1)) . 0 is ext-real Element of ExtREAL
(M * C1) . 0 is ext-real Element of ExtREAL
dom (M * C1) is V59() V60() V61() V62() V63() V64() Element of bool NAT

(M * C1) . D2 is ext-real Element of ExtREAL

C1 . D2 is Element of S

B2 . D2 is Element of S
D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
B2 . (D2 + 1) is Element of S
A . (D2 + 1) is Element of S
(A . (D2 + 1)) \/ (B2 . D2) is Element of S

(Ser (M * A)) . D2 is ext-real Element of ExtREAL
(Ser (M * C1)) . D2 is ext-real Element of ExtREAL
B2 . D2 is Element of S
M . (B2 . D2) is ext-real Element of ExtREAL
SUM (M * C1) is ext-real Element of ExtREAL
(Ser (M * C1)) . 1 is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative V90(X,S) Element of bool
A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) V53() Element of bool [:NAT,S:]
M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
SUM (M * A) is ext-real Element of ExtREAL
(X,S,A) is non empty V47() N_Measure_fam of S
union (X,S,A) is Element of S
M . (union (X,S,A)) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
A is Element of bool X

M . B is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
A is set
M . A is ext-real Element of ExtREAL
B is set
M . B is ext-real Element of ExtREAL
B is set
B2 is set
A is (X,S,M)
B2 \/ A is set
bool X is non empty Element of bool (bool X)
A is set
B is set
B2 is set
B2 is set
C2 is (X,S,M)
B2 \/ C2 is set
B2 is set
C2 is set
C1 is (X,S,M)
C2 \/ C1 is set
B2 is set
C2 is (X,S,M)
B2 \/ C2 is set
B is set
B is non empty Element of bool (bool X)
B2 is set
C1 is set
C2 is set
D2 is (X,S,M)
C1 \/ D2 is set
A is non empty Element of bool (bool X)
B is non empty Element of bool (bool X)
B2 is set
C2 is set
C1 is (X,S,M)
C2 \/ C1 is set
C2 is set
C1 is (X,S,M)
C2 \/ C1 is set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
(X,S,M) is non empty Element of bool (bool X)
A is Element of (X,S,M)
bool X is non empty Element of bool (bool X)
B is set
B2 is set
A \ B2 is Element of bool X
C2 is set
A \ C2 is Element of bool X
B2 is set
B2 is set
C2 is (X,S,M)
B2 \/ C2 is set
C2 is (X,S,M)
B2 \/ C2 is set
C1 is set
M . C1 is ext-real Element of ExtREAL
A \ B2 is Element of bool X
C2 \ B2 is Element of bool X
B2 is non empty Element of bool (bool X)
C2 is set
A \ C2 is Element of bool X
C1 is set
A \ C1 is Element of bool X
B is non empty Element of bool (bool X)
B2 is non empty Element of bool (bool X)
C2 is set
A \ C2 is Element of bool X
A \ C2 is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
(X,S,M) is non empty Element of bool (bool X)
[:NAT,(X,S,M):] is non empty set
bool [:NAT,(X,S,M):] is non empty set
A is V1() V4( NAT ) V5((X,S,M)) Function-like non empty V14( NAT ) V30( NAT ,(X,S,M)) Element of bool [:NAT,(X,S,M):]

A . B is Element of (X,S,M)
(X,S,M,(A . B)) is non empty Element of bool (bool X)
the Element of (X,S,M,(A . B)) is Element of (X,S,M,(A . B))
C2 is Element of S

D2 is set
A . C1 is Element of (X,S,M)
(X,S,M,(A . C1)) is non empty Element of bool (bool X)
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B . B2 is Element of S
A . B2 is Element of (X,S,M)
(X,S,M,(A . B2)) is non empty Element of bool (bool X)
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
(X,S,M) is non empty Element of bool (bool X)
[:NAT,(X,S,M):] is non empty set
bool [:NAT,(X,S,M):] is non empty set
A is V1() V4( NAT ) V5((X,S,M)) Function-like non empty V14( NAT ) V30( NAT ,(X,S,M)) Element of bool [:NAT,(X,S,M):]
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . B2 is Element of (X,S,M)
B . B2 is Element of S
(A . B2) \ (B . B2) is Element of bool (A . B2)
bool (A . B2) is non empty set
C2 is Element of bool X

D2 is set
A . C1 is Element of (X,S,M)
B . C1 is Element of S
(A . C1) \ (B . C1) is Element of bool (A . C1)
bool (A . C1) is non empty set
B2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]
B2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

B2 . C2 is Element of bool X
A . C2 is Element of (X,S,M)
B . C2 is Element of S
(A . C2) \ (B . C2) is Element of bool (A . C2)
bool (A . C2) is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
A is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

A . B is Element of bool X
B2 is set
M . B2 is ext-real Element of ExtREAL
C2 is Element of S

D2 is set
A . C1 is Element of bool X
M . D2 is ext-real Element of ExtREAL
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . B2 is Element of bool X
B . B2 is Element of S

B . C2 is Element of S
M . (B . C2) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
A is non empty Element of bool (bool X)
B is non empty V47() Element of bool (bool X)
union B is Element of bool X
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
B2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]
rng B2 is Element of bool (bool X)
bool (bool X) is non empty set

B2 . C2 is Element of bool X

B2 . C2 is Element of bool X
(X,S,M) is non empty Element of bool (bool X)

B2 . C2 is Element of bool X
C1 is set
D2 is (X,S,M)
C1 \/ D2 is set
C2 is set
B2 . C2 is set
dom B2 is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
[:NAT,(X,S,M):] is non empty set
bool [:NAT,(X,S,M):] is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
C2 is V1() V4( NAT ) V5((X,S,M)) Function-like non empty V14( NAT ) V30( NAT ,(X,S,M)) Element of bool [:NAT,(X,S,M):]
C1 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
D2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

C1 . O is Element of S
C2 . O is Element of (X,S,M)
(C2 . O) \ (C1 . O) is Element of bool (C2 . O)
bool (C2 . O) is non empty set
(X,S,M,(C2 . O)) is non empty Element of bool (bool X)

D2 . O is Element of bool X
C2 . O is Element of (X,S,M)
C1 . O is Element of S
(C2 . O) \ (C1 . O) is Element of bool (C2 . O)
bool (C2 . O) is non empty set
O is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
(X,S,C1) is non empty V47() N_Measure_fam of S
union (X,S,C1) is Element of S
rng C2 is Element of bool (X,S,M)
bool (X,S,M) is non empty set
union (rng C2) is set
D2 is set
O1 is set
dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT
c14 is set
C1 . c14 is set
c15 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
C2 . c15 is Element of (X,S,M)
C1 . c15 is Element of S
n is set
(X,S,O) is non empty V47() N_Measure_fam of S
D2 is set
dom O is V59() V60() V61() V62() V63() V64() Element of bool NAT
O1 is Element of S
M . O1 is ext-real Element of ExtREAL
c14 is set
O . c14 is set
union (X,S,O) is Element of S
M . (union (X,S,O)) is ext-real Element of ExtREAL
() \ (union (X,S,C1)) is Element of bool X
(union (rng C2)) /\ (union (X,S,C1)) is Element of bool X
(() \ (union (X,S,C1))) \/ ((union (rng C2)) /\ (union (X,S,C1))) is Element of bool X
(union (X,S,C1)) \/ (() \ (union (X,S,C1))) is Element of bool X
O1 is Element of bool X
rng D2 is Element of bool (bool X)
union (rng D2) is Element of bool X
c14 is set
c15 is set
n is set
C2 . n is set

C1 . n is Element of S
dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT
C2 . n is Element of (X,S,M)
(C2 . n) \ (C1 . n) is Element of bool (C2 . n)
bool (C2 . n) is non empty set
D2 . n is Element of bool X
dom D2 is V59() V60() V61() V62() V63() V64() Element of bool NAT
c18 is set
c14 is set
c15 is set
dom D2 is V59() V60() V61() V62() V63() V64() Element of bool NAT
n is set
D2 . n is set

dom O is V59() V60() V61() V62() V63() V64() Element of bool NAT
O . n is Element of S
D2 . n is Element of bool X
c14 is (X,S,M)
(union (X,S,C1)) \/ c14 is Element of bool X
D2 is (X,S,M)
(union (X,S,C1)) \/ D2 is Element of bool X
B2 is set
D2 is (X,S,M)
B2 \/ D2 is set
B is set
X \ B is Element of bool X
B2 is set
X \ B2 is Element of bool X
C1 is (X,S,M)
B2 \/ C1 is set
C1 is (X,S,M)
B2 \/ C1 is set
D2 is set
M . D2 is ext-real Element of ExtREAL
(X \ B2) \ D2 is Element of bool X
(X \ B2) \ C1 is Element of bool X
D2 \ C1 is Element of bool D2
bool D2 is non empty set
(X \ B2) /\ (D2 \ C1) is Element of bool D2
D2 is Element of bool X
O1 is (X,S,M)
((X \ B2) \ D2) \/ O1 is Element of bool X
B2 is (X,S,M)
((X \ B2) \ D2) \/ B2 is Element of bool X
B2 is set
C2 is (X,S,M)
B2 \/ C2 is set
B is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
(X,S,M) is non empty Element of bool (bool X)
A is set
B2 is set
B is set
C2 is (X,S,M)
B2 \/ C2 is set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
A is set
B is set
M . A is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
B2 is (X,S,M)
A \/ B2 is set
C2 is (X,S,M)
B \/ C2 is set
C1 is set
M . C1 is ext-real Element of ExtREAL
A \/ C1 is set
D2 is set
M . D2 is ext-real Element of ExtREAL
B \/ D2 is set
O is Element of S
D2 is Element of S
O \/ D2 is Element of S
M . (O \/ D2) is ext-real Element of ExtREAL
M . O is ext-real Element of ExtREAL
M . D2 is ext-real Element of ExtREAL
(M . O) + (M . D2) is ext-real Element of ExtREAL
B2 is Element of S
M . B2 is ext-real Element of ExtREAL
O1 is Element of S
B2 \/ O1 is Element of S
M . (B2 \/ O1) is ext-real Element of ExtREAL
M . O1 is ext-real Element of ExtREAL
(M . B2) + (M . O1) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
is non empty V67() set
bool is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool
(X,S,M) is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:(X,S,M),ExtREAL:] is non empty V67() set
bool [:(X,S,M),ExtREAL:] is non empty set

B2 is set
M . B2 is ext-real Element of ExtREAL
B2 is set
C2 is set
M . C2 is ext-real Element of ExtREAL
C1 is set
D2 is set
O is set
B2 is (X,S,M)
O \/ B2 is set
M . O is ext-real Element of ExtREAL
D2 is (X,S,M)
C2 \/ D2 is set
B2 is V1() V4((X,S,M)) V5( ExtREAL ) Function-like non empty V14((X,S,M)) V30((X,S,M), ExtREAL ) V67() Element of bool [:(X,S,M),ExtREAL:]
C2 is set
M . C2 is ext-real Element of ExtREAL
C1 is (X,S,M)
C2 \/ C1 is set
B2 . (C2 \/ C1) is ext-real Element of ExtREAL
[:NAT,(X,S,M):] is non empty set
bool [:NAT,(X,S,M):] is non empty set
C2 is V1() V4( NAT ) V5((X,S,M)) Function-like non empty V14( NAT ) V30( NAT ,(X,S,M)) V53() Element of bool [:NAT,(X,S,M):]
B2 * C2 is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool
SUM (B2 * C2) is ext-real Element of ExtREAL
(X,(X,S,M),C2) is non empty V47() N_Measure_fam of (X,S,M)
union (X,(X,S,M),C2) is Element of (X,S,M)
B2 . (union (X,(X,S,M),C2)) is ext-real Element of ExtREAL
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
C1 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
D2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

C1 . O is Element of S
C2 . O is Element of (X,S,M)
(C2 . O) \ (C1 . O) is Element of bool (C2 . O)
bool (C2 . O) is non empty set
(X,S,M,(C2 . O)) is non empty Element of bool (bool X)

D2 . O is Element of bool X
C2 . O is Element of (X,S,M)
C1 . O is Element of S
(C2 . O) \ (C1 . O) is Element of bool (C2 . O)
bool (C2 . O) is non empty set
O is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]
B2 is set
D2 is set
C1 . B2 is set
C1 . D2 is set
dom C2 is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT
O1 is set
C1 . O1 is set
C2 . O1 is set
C2 . B2 is set
C2 . D2 is set
(C2 . B2) /\ (C2 . D2) is set
(C1 . B2) /\ (C1 . D2) is set
(X,S,C1) is non empty V47() N_Measure_fam of S
union (X,S,C1) is Element of S
B2 is set
dom C2 is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool NAT is non empty set
D2 is set
O1 is set
dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT
c14 is set
C1 . c14 is set
c15 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
C2 . c15 is Element of (X,S,M)
C1 . c15 is Element of S
n is set
(X,S,O) is non empty V47() N_Measure_fam of S
D2 is set
dom O is V59() V60() V61() V62() V63() V64() Element of bool NAT
O1 is Element of S
M . O1 is ext-real Element of ExtREAL
c14 is set
O . c14 is set
union (X,S,O) is Element of S
M . (union (X,S,O)) is ext-real Element of ExtREAL
(union (X,(X,S,M),C2)) \ B2 is Element of bool X
(union (X,(X,S,M),C2)) /\ B2 is Element of bool X
((union (X,(X,S,M),C2)) \ B2) \/ ((union (X,(X,S,M),C2)) /\ B2) is Element of bool X
B2 \/ ((union (X,(X,S,M),C2)) \ B2) is set
O1 is Element of bool X
rng D2 is Element of bool (bool X)
bool (bool X) is non empty set
union (rng D2) is Element of bool X
c14 is set
c15 is set
n is set
C2 . n is set

C1 . n is Element of S
dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT
C2 . n is Element of (X,S,M)
(C2 . n) \ (C1 . n) is Element of bool (C2 . n)
bool (C2 . n) is non empty set
D2 . n is Element of bool X
dom D2 is V59() V60() V61() V62() V63() V64() Element of bool NAT
c18 is set
c14 is set
c15 is set
dom D2 is V59() V60() V61() V62() V63() V64() Element of bool NAT
n is set
D2 . n is set

dom O is V59() V60() V61() V62() V63() V64() Element of bool NAT
O . n is Element of S
D2 . n is Element of bool X
c14 is (X,S,M)
B2 \/ c14 is set
D2 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) V53() Element of bool [:NAT,S:]

C2 . O1 is Element of (X,S,M)
B2 . (C2 . O1) is ext-real Element of ExtREAL
D2 . O1 is Element of S
M . (D2 . O1) is ext-real Element of ExtREAL
(C2 . O1) \ (D2 . O1) is Element of bool (C2 . O1)
bool (C2 . O1) is non empty set
c14 is (X,S,M)
(C2 . O1) /\ (D2 . O1) is set