:: PROB_4 semantic presentation

REAL is non empty V44() V50() V51() V52() V56() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() Element of bool REAL

bool REAL is non empty V79() set

ExtREAL is non empty V51() set

[:NAT,ExtREAL:] is non empty V13() V34() set

bool [:NAT,ExtREAL:] is non empty V79() set

bool ExtREAL is non empty V79() set

COMPLEX is non empty V44() V50() V56() set

RAT is non empty V44() V50() V51() V52() V53() V56() set

INT is non empty V44() V50() V51() V52() V53() V54() V56() set

[:NAT,REAL:] is non empty V13() V33() V34() V35() set

bool [:NAT,REAL:] is non empty V79() set

omega is non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() set

bool omega is non empty V79() set

bool (bool REAL) is non empty V79() set

{} is set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() V13() non-empty empty-yielding V17( RAT ) ext-real non positive non negative V33() V34() V35() V36() V50() V51() V52() V53() V54() V55() V56() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() V13() non-empty empty-yielding V17( RAT ) ext-real non positive non negative V33() V34() V35() V36() V50() V51() V52() V53() V54() V55() V56() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

{{},1} is V79() set

bool NAT is non empty V79() set

0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

0. is ext-real Element of ExtREAL

+infty is non empty V12() ext-real positive non negative Element of ExtREAL

+infty is non empty V12() ext-real positive non negative set

-infty is non empty V12() ext-real non positive negative set

{-infty} is V51() set

{+infty} is V51() set

P is set

Sigma is set

Omega is set

Omega \ P is Element of bool Omega

bool Omega is non empty V79() set

Omega \ Sigma is Element of bool Omega

Sigma \ P is Element of bool Sigma

bool Sigma is non empty V79() set

Omega /\ (Sigma \ P) is Element of bool Sigma

(Omega \ Sigma) \/ (Omega /\ (Sigma \ P)) is set

A is set

A is set

Omega is set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

P . A is set

P . A is Event of Sigma

Omega is set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng P is non empty Element of bool (bool Omega)

A is set

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,P,B) is Element of Sigma

Omega is set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,Sigma:] is non empty V13() set

bool [:NAT,Sigma:] is non empty V79() set

P is V13() Function-like set

A is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng A is non empty Element of bool (bool Omega)

dom A is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT

A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

F

bool F

bool (bool F

F

bool F

[:NAT,(bool F

bool [:NAT,(bool F

Omega is non empty V13() V16( NAT ) V17( bool F

Omega is non empty V13() V16( NAT ) V17( bool F

Sigma is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set

Omega . Sigma is set

F

rng Omega is non empty Element of bool (bool F

Sigma is non empty V13() V16( NAT ) V17(F

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(F

F

Omega is set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

{} Omega is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() V13() non-empty empty-yielding V17( RAT ) ext-real non positive non negative V33() V34() V35() V36() V50() V51() V52() V53() V54() V55() V56() Element of bool Omega

NAT --> ({} Omega) is non empty T-Sequence-like V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) V33() V34() V35() V36() Element of bool [:NAT,(bool Omega):]

Sigma is non empty T-Sequence-like V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) V33() V34() V35() V36() Element of bool [:NAT,(bool Omega):]

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set

Sigma . P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set

Sigma . A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set

Omega is set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

P is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,P:] is non empty V13() set

bool [:NAT,P:] is non empty V79() set

the non empty V13() V16( NAT ) V17(P) Function-like V23( NAT ) V27( NAT ,P) disjoint_valued Element of bool [:NAT,P:] is non empty V13() V16( NAT ) V17(P) Function-like V23( NAT ) V27( NAT ,P) disjoint_valued Element of bool [:NAT,P:]

B is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Omega is set

bool Omega is non empty V79() set

Sigma is Element of bool Omega

P is Element of bool Omega

(Sigma,P) followed_by {} is V13() Function-like set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool (bool Omega) is non empty V79() set

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

{} Omega is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() V13() non-empty empty-yielding V17( RAT ) ext-real non positive non negative V33() V34() V35() V36() V50() V51() V52() V53() V54() V55() V56() Element of bool Omega

(Sigma,P) followed_by ({} Omega) is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

(Omega,(bool Omega),A,1) is Element of bool Omega

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set

C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set

A . B is set

A . C is set

(Omega,(bool Omega),A,0) is Element of bool Omega

C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

B + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

Omega is set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty set

P is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng A is non empty Element of bool (bool Omega)

Union A is Element of bool Omega

B is non empty V13() V16( NAT ) V17( bool Omega) V17(P) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Union B is Element of bool Omega

A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng A is non empty Element of bool (bool Omega)

Union A is Element of bool Omega

B is Element of bool Omega

B ` is Element of bool Omega

Omega \ B is set

P is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng P is non empty Element of bool (bool Omega)

Intersection P is Element of bool Omega

Complement P is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative set

(Complement P) . A is set

P . A is set

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),P,B) is Element of bool Omega

(Omega,(bool Omega),P,B) ` is Element of bool Omega

Omega \ (Omega,(bool Omega),P,B) is set

rng (Complement P) is non empty Element of bool (bool Omega)

Union (Complement P) is Element of bool Omega

(Union (Complement P)) ` is Element of bool Omega

Omega \ (Union (Complement P)) is set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

A is Event of Sigma

B is Event of Sigma

A \ B is Element of Sigma

P . (A \ B) is V11() V12() ext-real Element of REAL

A \/ B is Element of Sigma

P . (A \/ B) is V11() V12() ext-real Element of REAL

P . B is V11() V12() ext-real Element of REAL

(P . (A \/ B)) - (P . B) is V11() V12() ext-real Element of REAL

(P . B) + (P . (A \ B)) is V11() V12() ext-real Element of REAL

((P . B) + (P . (A \ B))) - (P . B) is V11() V12() ext-real Element of REAL

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

A is Event of Sigma

B is Event of Sigma

P . B is V11() V12() ext-real Element of REAL

P . A is V11() V12() ext-real Element of REAL

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Union P is Element of bool Omega

A is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

A . (Union P) is V11() V12() ext-real set

A * P is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

Partial_Sums (A * P) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Partial_Sums (A * P)) . B is V11() V12() ext-real Element of REAL

B + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Partial_Sums (A * P)) . (B + 1) is V11() V12() ext-real Element of REAL

(A * P) . (B + 1) is V11() V12() ext-real Element of REAL

((Partial_Sums (A * P)) . B) + ((A * P) . (B + 1)) is V11() V12() ext-real Element of REAL

(Omega,Sigma,P,(B + 1)) is Element of Sigma

A . (Omega,Sigma,P,(B + 1)) is V11() V12() ext-real Element of REAL

0 + (A . (Omega,Sigma,P,(B + 1))) is V11() V12() ext-real Element of REAL

(Partial_Sums (A * P)) . 0 is V11() V12() ext-real Element of REAL

(A * P) . 0 is V11() V12() ext-real Element of REAL

(Omega,Sigma,P,0) is Element of Sigma

A . (Omega,Sigma,P,0) is V11() V12() ext-real Element of REAL

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Partial_Sums (A * P)) . B is V11() V12() ext-real Element of REAL

lim (Partial_Sums (A * P)) is V11() V12() ext-real Element of REAL

Partial_Diff_Union P is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,(Partial_Diff_Union P),B) is Element of Sigma

(Omega,Sigma,P,B) is Element of Sigma

A * (Partial_Diff_Union P) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

(A * (Partial_Diff_Union P)) . B is V11() V12() ext-real Element of REAL

(A * P) . B is V11() V12() ext-real Element of REAL

Partial_Sums (A * (Partial_Diff_Union P)) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Partial_Sums (A * (Partial_Diff_Union P))) . B is V11() V12() ext-real Element of REAL

(Partial_Sums (A * P)) . B is V11() V12() ext-real Element of REAL

Sum (A * (Partial_Diff_Union P)) is V11() V12() ext-real Element of REAL

lim (Partial_Sums (A * (Partial_Diff_Union P))) is V11() V12() ext-real Element of REAL

Union (Partial_Diff_Union P) is Element of bool Omega

A . (Union (Partial_Diff_Union P)) is V11() V12() ext-real set

C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,P,C) is Element of Sigma

rng P is non empty Element of bool (bool Omega)

union (rng P) is Element of bool Omega

B is Event of Sigma

B is Event of Sigma

A . (Omega,Sigma,P,C) is V11() V12() ext-real Element of REAL

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng P is non empty Element of bool (bool Omega)

union (rng P) is Element of bool Omega

A is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

A . (union (rng P)) is V11() V12() ext-real set

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,P,B) is Element of Sigma

A . (Omega,Sigma,P,B) is V11() V12() ext-real Element of REAL

Union P is Element of bool Omega

A . (Union P) is V11() V12() ext-real set

B is set

A . B is V11() V12() ext-real set

C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,P,C) is Element of Sigma

Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

Partial_Sums Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]

Ser Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]

P is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

P . A is ext-real Element of ExtREAL

(Ser Sigma) . A is ext-real Element of ExtREAL

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

P . (A + 1) is ext-real Element of ExtREAL

(Ser Sigma) . (A + 1) is ext-real Element of ExtREAL

(Partial_Sums Omega) . A is V11() V12() ext-real Element of REAL

B is V11() V12() ext-real Element of REAL

Omega . (A + 1) is V11() V12() ext-real Element of REAL

B + (Omega . (A + 1)) is V11() V12() ext-real Element of REAL

Sigma . (A + 1) is ext-real Element of ExtREAL

((Ser Sigma) . A) + (Sigma . (A + 1)) is ext-real Element of ExtREAL

P . 0 is ext-real Element of ExtREAL

Sigma . 0 is ext-real Element of ExtREAL

(Ser Sigma) . 0 is ext-real Element of ExtREAL

Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

upper_bound Omega is V11() V12() ext-real Element of REAL

Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]

rng Sigma is non empty V51() Element of bool ExtREAL

sup (rng Sigma) is ext-real set

dom Sigma is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT

-infty is non empty V12() ext-real non positive negative Element of ExtREAL

{-infty} is V51() set

A is ext-real Element of rng Sigma

B is set

Sigma . B is ext-real set

C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

Omega . C is V11() V12() ext-real Element of REAL

P is ext-real Element of ExtREAL

A is ext-real set

B is set

Sigma . B is ext-real set

A is V11() V12() ext-real Element of REAL

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

Omega . B is V11() V12() ext-real Element of REAL

Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

lower_bound Omega is V11() V12() ext-real Element of REAL

Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]

rng Sigma is non empty V51() Element of bool ExtREAL

inf (rng Sigma) is ext-real set

dom Sigma is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT

{+infty} is V51() set

A is ext-real Element of rng Sigma

B is set

Sigma . B is ext-real set

C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

Omega . C is V11() V12() ext-real Element of REAL

P is ext-real Element of ExtREAL

A is ext-real set

B is set

Sigma . B is ext-real set

A is V11() V12() ext-real Element of REAL

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

Omega . B is V11() V12() ext-real Element of REAL

Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

Sum Omega is V11() V12() ext-real Element of REAL

Partial_Sums Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

lim (Partial_Sums Omega) is V11() V12() ext-real Element of REAL

Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]

SUM Sigma is ext-real Element of ExtREAL

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

Omega . P is V11() V12() ext-real Element of REAL

upper_bound (Partial_Sums Omega) is V11() V12() ext-real Element of REAL

Ser Sigma is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]

rng (Ser Sigma) is non empty V51() Element of bool ExtREAL

sup (rng (Ser Sigma)) is ext-real set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:Sigma,ExtREAL:] is non empty V13() V34() set

bool [:Sigma,ExtREAL:] is non empty V79() set

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

B is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() Element of bool [:Sigma,ExtREAL:]

rng B is non empty V51() Element of bool ExtREAL

C is ext-real Element of ExtREAL

dom B is non empty Element of bool Sigma

bool Sigma is non empty V79() set

B is set

B . B is ext-real set

A is Event of Sigma

P . A is V11() V12() ext-real Element of REAL

[:NAT,Sigma:] is non empty V13() set

bool [:NAT,Sigma:] is non empty V79() set

C is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) disjoint_valued Element of bool [:NAT,Sigma:]

B * C is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]

SUM (B * C) is ext-real Element of ExtREAL

rng C is non empty Element of bool (bool Omega)

union (rng C) is Element of bool Omega

B . (union (rng C)) is ext-real set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

B is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]

P * B is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(P * B) . A is V11() V12() ext-real Element of REAL

Partial_Sums (P * B) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

Union B is Element of bool Omega

P . (Union B) is V11() V12() ext-real set

Sum (P * B) is V11() V12() ext-real Element of REAL

lim (Partial_Sums (P * B)) is V11() V12() ext-real Element of REAL

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

[:Sigma,ExtREAL:] is non empty V13() V34() set

bool [:Sigma,ExtREAL:] is non empty V79() set

R_EAL 1 is ext-real Element of ExtREAL

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:Sigma,ExtREAL:] is non empty V13() V34() set

bool [:Sigma,ExtREAL:] is non empty V79() set

P is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]

P . Omega is ext-real set

B is Element of Sigma

P . B is ext-real Element of ExtREAL

A is Element of Sigma

P . A is ext-real Element of ExtREAL

A is set

P . A is ext-real set

B is Element of Sigma

P . B is ext-real Element of ExtREAL

dom P is non empty Element of bool Sigma

bool Sigma is non empty V79() set

[:Sigma,REAL:] is non empty V13() V33() V34() V35() set

bool [:Sigma,REAL:] is non empty V79() set

A is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() Element of bool [:Sigma,REAL:]

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

B is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() Element of bool [:Sigma,REAL:]

C is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

B * C is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]

lim (B * C) is V11() V12() ext-real Element of REAL

Intersection C is Element of bool Omega

B . (Intersection C) is V11() V12() ext-real set

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(B * C) . B is V11() V12() ext-real Element of REAL

(Omega,Sigma,C,B) is Element of Sigma

A is Event of Sigma

B . A is V11() V12() ext-real Element of REAL

dom (B * C) is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT

[:NAT,Sigma:] is non empty V13() set

bool [:NAT,Sigma:] is non empty V79() set

B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

B . (A + 1) is Element of Sigma

B . A is Element of Sigma

B . 0 is Element of Sigma

P . (B . 0) is ext-real Element of ExtREAL

P * B is non empty V13() V16( NAT ) V17( ExtREAL ) Function-like V23( NAT ) V27( NAT , ExtREAL ) V34() Element of bool [:NAT,ExtREAL:]

dom (P * B) is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(P * B) . A is ext-real Element of ExtREAL

B . A is Element of Sigma

P . (B . A) is ext-real Element of ExtREAL

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(P * B) . (A + 1) is ext-real Element of ExtREAL

B . (A + 1) is Element of Sigma

P . (B . (A + 1)) is ext-real Element of ExtREAL

(B * C) . (A + 1) is V11() V12() ext-real Element of REAL

(B * C) . A is V11() V12() ext-real Element of REAL

lower_bound (B * C) is V11() V12() ext-real Element of REAL

rng (P * B) is non empty V51() Element of bool ExtREAL

inf (rng (P * B)) is ext-real set

rng B is non empty Element of bool (bool Omega)

meet (rng B) is Element of bool Omega

P . (meet (rng B)) is ext-real set

C is Event of Sigma

B is Event of Sigma

C \/ B is Element of Sigma

B . (C \/ B) is V11() V12() ext-real Element of REAL

B . C is V11() V12() ext-real Element of REAL

B . B is V11() V12() ext-real Element of REAL

(B . C) + (B . B) is V11() V12() ext-real Element of REAL

A is Element of Sigma

B is Element of Sigma

A \/ B is Element of Sigma

B . (A \/ B) is V11() V12() ext-real Element of REAL

O is Element of Sigma

P . O is ext-real Element of ExtREAL

B2 is Element of Sigma

P . B2 is ext-real Element of ExtREAL

(P . O) + (P . B2) is ext-real Element of ExtREAL

B . A is V11() V12() ext-real Element of REAL

B . B is V11() V12() ext-real Element of REAL

(B . A) + (B . B) is V11() V12() ext-real Element of REAL

B . Omega is V11() V12() ext-real set

C is Event of Sigma

B . C is V11() V12() ext-real Element of REAL

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:Sigma,ExtREAL:] is non empty V13() V34() set

bool [:Sigma,ExtREAL:] is non empty V79() set

P is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]

P . Omega is ext-real set

Omega is set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Partial_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega

(Omega,(bool Omega),Sigma,P) is Element of bool Omega

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),(Partial_Union Sigma),(P + 1)) is Element of bool Omega

(Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega

(Omega,(bool Omega),Sigma,P) \/ (Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega

(Omega,(bool Omega),(Partial_Union Sigma),0) is Element of bool Omega

(Omega,(bool Omega),Sigma,0) is Element of bool Omega

Omega is set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Partial_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega

(Omega,(bool Omega),Sigma,P) is Element of bool Omega

Omega is set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Partial_Diff_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]

(Omega,(bool Omega),(Partial_Diff_Union Sigma),0) is Element of bool Omega

(Omega,(bool Omega),Sigma,0) is Element of bool Omega

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),(Partial_Diff_Union Sigma),(P + 1)) is Element of bool Omega

(Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega

(Omega,(bool Omega),Sigma,P) is Element of bool Omega

(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),Sigma,P) is Element of bool Omega

Partial_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

(Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega

(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega

Omega is set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Partial_Diff_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega

(Omega,(bool Omega),(Partial_Diff_Union Sigma),(P + 1)) is Element of bool Omega

(Omega,(bool Omega),Sigma,P) is Element of bool Omega

(Omega,(bool Omega),(Partial_Diff_Union Sigma),(P + 1)) \/ (Omega,(bool Omega),Sigma,P) is Element of bool Omega

Partial_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

(Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega

(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),(Partial_Union Sigma),P) is Element of bool Omega

((Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),(Partial_Union Sigma),P)) \/ (Omega,(bool Omega),Sigma,P) is Element of bool Omega

(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),Sigma,P) is Element of bool Omega

((Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),Sigma,P)) \/ (Omega,(bool Omega),Sigma,P) is Element of bool Omega

(Omega,(bool Omega),Sigma,(P + 1)) \/ (Omega,(bool Omega),Sigma,P) is Element of bool Omega

Omega is set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Partial_Diff_Union Sigma is non empty V13() V16( NAT ) V17( bool Omega) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]

P is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),(Partial_Diff_Union Sigma),(P + 1)) is Element of bool Omega

(Omega,(bool Omega),Sigma,P) is Element of bool Omega

(Omega,(bool Omega),Sigma,(P + 1)) is Element of bool Omega

(Omega,(bool Omega),Sigma,(P + 1)) \ (Omega,(bool Omega),Sigma,P) is Element of bool Omega

Omega is set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Partial_Union P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Omega is set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Partial_Diff_Union P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]

(Omega,Sigma,(Partial_Diff_Union P),0) is Element of Sigma

(Omega,Sigma,P,0) is Element of Sigma

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,(Partial_Diff_Union P),(A + 1)) is Element of Sigma

(Omega,Sigma,P,(A + 1)) is Element of Sigma

(Omega,Sigma,P,A) is Element of Sigma

(Omega,Sigma,P,(A + 1)) \ (Omega,Sigma,P,A) is Element of Sigma

Omega is set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

Partial_Diff_Union P is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) disjoint_valued Element of bool [:NAT,(bool Omega):]

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,(Partial_Diff_Union P),(A + 1)) is Element of Sigma

(Omega,Sigma,P,A) is Element of Sigma

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]

[:Sigma,ExtREAL:] is non empty V13() V34() set

bool [:Sigma,ExtREAL:] is non empty V79() set

B is set

A is Element of bool Omega

(Omega,Sigma,P) . B is ext-real set

B is set

A is Element of bool Omega

P . B is V11() V12() ext-real set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

A is Element of bool Omega

B is set

P . B is V11() V12() ext-real set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]

[:Sigma,ExtREAL:] is non empty V13() V34() set

bool [:Sigma,ExtREAL:] is non empty V79() set

A is Element of bool Omega

B is set

P . B is V11() V12() ext-real set

B is set

(Omega,Sigma,P) . B is ext-real set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

P . {} is V11() V12() ext-real set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

A is set

B is set

P . A is V11() V12() ext-real set

P . B is V11() V12() ext-real set

C is (Omega,Sigma,P)

A \/ C is set

B is (Omega,Sigma,P)

B \/ B is set

A is set

P . A is V11() V12() ext-real set

A \/ A is set

B is set

P . B is V11() V12() ext-real set

B \/ B is set

O is Event of Sigma

D2 is Event of Sigma

O \/ D2 is Element of Sigma

P . (O \/ D2) is V11() V12() ext-real Element of REAL

P . O is V11() V12() ext-real Element of REAL

P . D2 is V11() V12() ext-real Element of REAL

(P . O) + (P . D2) is V11() V12() ext-real Element of REAL

B2 is Event of Sigma

P . B2 is V11() V12() ext-real Element of REAL

c

B2 \/ c

P . (B2 \/ c

P . c

(P . B2) + (P . c

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

A is set

B is set

C is (Omega,Sigma,P)

B \/ C is set

A is set

B is set

C is set

C is set

B is (Omega,Sigma,P)

C \/ B is set

C is set

B is set

A is (Omega,Sigma,P)

B \/ A is set

C is set

B is (Omega,Sigma,P)

C \/ B is set

B is set

B is non empty Element of bool (bool Omega)

C is set

A is set

B is set

B is (Omega,Sigma,P)

A \/ B is set

A is non empty Element of bool (bool Omega)

B is non empty Element of bool (bool Omega)

C is set

B is set

A is (Omega,Sigma,P)

B \/ A is set

B is set

A is (Omega,Sigma,P)

B \/ A is set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

A is (Omega,Sigma,P)

B is Element of Sigma

B \/ A is Element of bool Omega

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]

[:Sigma,ExtREAL:] is non empty V13() V34() set

bool [:Sigma,ExtREAL:] is non empty V79() set

COM (Sigma,(Omega,Sigma,P)) is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

A is set

B is set

C is thin of (Omega,Sigma,P)

B \/ C is set

C is thin of (Omega,Sigma,P)

B \/ C is set

B is (Omega,Sigma,P)

B \/ B is set

A is set

B is set

C is (Omega,Sigma,P)

B \/ C is set

C is (Omega,Sigma,P)

B \/ C is set

B is thin of (Omega,Sigma,P)

B \/ B is set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

A is Element of (Omega,Sigma,P)

(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]

[:Sigma,ExtREAL:] is non empty V13() V34() set

bool [:Sigma,ExtREAL:] is non empty V79() set

COM (Sigma,(Omega,Sigma,P)) is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

B is set

A is (Omega,Sigma,P)

B \/ A is set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

A is Element of (Omega,Sigma,P)

B is set

C is set

A \ C is Element of bool Omega

B is set

A \ B is Element of bool Omega

C is set

C is set

B is (Omega,Sigma,P)

C \/ B is set

B is (Omega,Sigma,P)

C \/ B is set

A is set

P . A is V11() V12() ext-real set

A \ C is Element of bool Omega

B \ C is Element of bool Omega

C is non empty Element of bool (bool Omega)

B is set

A \ B is Element of bool Omega

A is set

A \ A is Element of bool Omega

B is non empty Element of bool (bool Omega)

C is non empty Element of bool (bool Omega)

B is set

A \ B is Element of bool Omega

A \ B is Element of bool Omega

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

(Omega,Sigma,P) is non empty V13() V16(Sigma) V17( ExtREAL ) Function-like V23(Sigma) V27(Sigma, ExtREAL ) V34() V42() nonnegative sigma-additive Element of bool [:Sigma,ExtREAL:]

[:Sigma,ExtREAL:] is non empty V13() V34() set

bool [:Sigma,ExtREAL:] is non empty V79() set

A is Element of (Omega,Sigma,P)

(Omega,Sigma,P,A) is non empty Element of bool (bool Omega)

(Omega,Sigma,P,A) is Element of COM (Sigma,(Omega,Sigma,P))

COM (Sigma,(Omega,Sigma,P)) is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

MeasPart (Omega,Sigma,P,A) is non empty Element of bool (bool Omega)

B is set

(Omega,Sigma,P,A) \ B is Element of bool Omega

A \ B is Element of bool Omega

B is set

A \ B is Element of bool Omega

(Omega,Sigma,P,A) \ B is Element of bool Omega

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

A is Element of (Omega,Sigma,P)

(Omega,Sigma,P,A) is non empty Element of bool (bool Omega)

B is set

C is set

P . B is V11() V12() ext-real set

P . C is V11() V12() ext-real set

A \ B is Element of bool Omega

A \ C is Element of bool Omega

B is (Omega,Sigma,P)

B \/ B is set

A is (Omega,Sigma,P)

C \/ A is set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

[:NAT,(Omega,Sigma,P):] is non empty V13() set

bool [:NAT,(Omega,Sigma,P):] is non empty V79() set

A is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) Function-like V23( NAT ) V27( NAT ,(Omega,Sigma,P)) Element of bool [:NAT,(Omega,Sigma,P):]

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

A . B is Element of (Omega,Sigma,P)

(Omega,Sigma,P,(A . B)) is non empty Element of bool (bool Omega)

the Element of (Omega,Sigma,P,(A . B)) is Element of (Omega,Sigma,P,(A . B))

B is Element of Sigma

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

B is set

A . A is Element of (Omega,Sigma,P)

(Omega,Sigma,P,(A . A)) is non empty Element of bool (bool Omega)

[:NAT,Sigma:] is non empty V13() set

bool [:NAT,Sigma:] is non empty V79() set

B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]

B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]

C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

B is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,B,A) is Element of Sigma

A . A is Element of (Omega,Sigma,P)

(Omega,Sigma,P,(A . A)) is non empty Element of bool (bool Omega)

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

[:NAT,(Omega,Sigma,P):] is non empty V13() set

bool [:NAT,(Omega,Sigma,P):] is non empty V79() set

A is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) Function-like V23( NAT ) V27( NAT ,(Omega,Sigma,P)) Element of bool [:NAT,(Omega,Sigma,P):]

B is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

C is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

A . C is Element of (Omega,Sigma,P)

(Omega,Sigma,B,C) is Element of Sigma

(A . C) \ (Omega,Sigma,B,C) is Element of bool (A . C)

bool (A . C) is non empty V79() set

B is Element of bool Omega

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

B is set

A . A is Element of (Omega,Sigma,P)

(Omega,Sigma,B,A) is Element of Sigma

(A . A) \ (Omega,Sigma,B,A) is Element of bool (A . A)

bool (A . A) is non empty V79() set

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),C,B) is Element of bool Omega

A . B is Element of (Omega,Sigma,P)

(Omega,Sigma,B,B) is Element of Sigma

(A . B) \ (Omega,Sigma,B,B) is Element of bool (A . B)

bool (A . B) is non empty V79() set

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

A is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),A,B) is Element of bool Omega

C is set

P . C is V11() V12() ext-real set

B is Element of Sigma

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

B is set

(Omega,(bool Omega),A,A) is Element of bool Omega

P . B is V11() V12() ext-real set

[:NAT,Sigma:] is non empty V13() set

bool [:NAT,Sigma:] is non empty V79() set

B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]

B is non empty V13() V16( NAT ) V17(Sigma) Function-like V23( NAT ) V27( NAT ,Sigma) Element of bool [:NAT,Sigma:]

C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

B is non empty V13() V16( NAT ) V17( bool Omega) V17(Sigma) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

A is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,(bool Omega),A,A) is Element of bool Omega

(Omega,Sigma,B,A) is Element of Sigma

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,B,B) is Element of Sigma

P . (Omega,Sigma,B,B) is V11() V12() ext-real Element of REAL

Omega is non empty set

bool Omega is non empty V79() set

bool (bool Omega) is non empty V79() set

Sigma is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

P is non empty V13() V16(Sigma) V17( REAL ) Function-like V23(Sigma) V27(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma

A is non empty Element of bool (bool Omega)

bool Omega is non empty compl-closed sigma-multiplicative V78() V79() V80() sigma-additive Element of bool (bool Omega)

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

B is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

rng B is non empty Element of bool (bool Omega)

Union B is Element of bool Omega

[:NAT,(bool Omega):] is non empty V13() set

bool [:NAT,(bool Omega):] is non empty V79() set

C is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

dom C is non empty V50() V51() V52() V53() V54() V55() Element of bool NAT

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

C . B is Element of bool Omega

rng C is non empty Element of bool (bool Omega)

(Omega,Sigma,P) is non empty Element of bool (bool Omega)

B is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

C . B is Element of bool Omega

A is set

B is (Omega,Sigma,P)

A \/ B is set

B is set

C . B is set

[:NAT,(Omega,Sigma,P):] is non empty V13() set

bool [:NAT,(Omega,Sigma,P):] is non empty V79() set

B is non empty V13() V16( NAT ) V17((Omega,Sigma,P)) Function-like V23( NAT ) V27( NAT ,(Omega,Sigma,P)) Element of bool [:NAT,(Omega,Sigma,P):]

A is non empty V13() V16( NAT ) V17(Sigma) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

B is non empty V13() V16( NAT ) V17( bool Omega) Function-like V23( NAT ) V27( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]

O is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT

(Omega,Sigma,A,O) is Element of Sigma

B . O is Element of (Omega,Sigma,P)

(B . O) \ (Omega,Sigma,A,O) is Element of bool (B . O)

bool (B . O) is non empty V79() set

(Omega,Sigma,P,(B . O)) is non empty