:: QMAX_1 semantic presentation

REAL is non empty V57() V131() V132() V133() V137() set

NAT is non empty V36() V37() V38() V131() V132() V133() V134() V135() V136() V137() Element of bool REAL

bool REAL is non empty V143() set

NAT is non empty V36() V37() V38() V131() V132() V133() V134() V135() V136() V137() set

bool NAT is non empty V143() set

[:NAT,REAL:] is non empty Relation-like set

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

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

COMPLEX is non empty V57() V131() V137() set

RAT is non empty V57() V131() V132() V133() V134() V137() set

INT is non empty V57() V131() V132() V133() V134() V135() V137() set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V36() V37() V38() V40() V41() V42() V131() V132() V133() V134() V135() V136() V137() set

1 is non empty ext-real positive V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional ext-real V36() V37() V38() V40() V41() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() V137() Element of NAT

Borel_Sets is non empty compl-closed sigma-multiplicative V143() Element of bool (bool REAL)

X is non empty set

bool X is non empty V143() set

bool (bool X) is non empty V143() set

P is non empty compl-closed sigma-multiplicative V143() Element of bool (bool X)

Funcs (P,REAL) is non empty FUNCTION_DOMAIN of P, REAL

P is set

f is set

P is set

f is set

Y is set

X is non empty set

bool X is non empty V143() set

bool (bool X) is non empty V143() set

P is non empty compl-closed sigma-multiplicative V143() Element of bool (bool X)

(X,P) is set

the Relation-like P -defined REAL -valued Function-like quasi_total V54() Probability of P is Relation-like P -defined REAL -valued Function-like quasi_total V54() Probability of P

(REAL,Borel_Sets) is non empty set

X is ()

the of X is non empty set

the of X is non empty set

X is ()

(X) is set

the of X is non empty set

(X) is set

the of X is non empty set

K105(REAL) is non empty compl-closed sigma-multiplicative V143() Element of bool (bool REAL)

[:NAT,K105(REAL):] is non empty Relation-like set

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

X is ()

(X) is non empty set

the of X is non empty set

(X) is non empty set

the of X is non empty set

the of X is Relation-like [: the of X, the of X:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of X, the of X:],(REAL,Borel_Sets):]

[: the of X, the of X:] is non empty Relation-like set

[:[: the of X, the of X:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of X, the of X:],(REAL,Borel_Sets):] is non empty V143() set

P is Element of (X)

P is Element of (X)

[P,P] is V1() Element of [:(X),(X):]

[:(X),(X):] is non empty Relation-like set

the of X . [P,P] is set

f is Element of [: the of X, the of X:]

the of X . f is Element of (REAL,Borel_Sets)

{0} is non empty functional V131() V132() V133() V134() V135() V136() Element of bool NAT

bool NAT is non empty V143() set

[:Borel_Sets,REAL:] is non empty Relation-like set

bool [:Borel_Sets,REAL:] is non empty V143() set

P is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total Element of bool [:Borel_Sets,REAL:]

P is Event of Borel_Sets

P . P is ext-real V43() V44() Element of REAL

P . REAL is set

[#] REAL is non empty non proper V131() V132() V133() Element of bool REAL

P is Event of Borel_Sets

P . P is ext-real V43() V44() Element of REAL

f is Event of Borel_Sets

P \/ f is Event of Borel_Sets

P . (P \/ f) is ext-real V43() V44() Element of REAL

P . f is ext-real V43() V44() Element of REAL

(P . P) + (P . f) is ext-real V43() V44() Element of REAL

P is Relation-like NAT -defined Borel_Sets -valued K105(REAL) -valued Function-like quasi_total Element of bool [:NAT,K105(REAL):]

P * P is Relation-like NAT -defined REAL -valued Function-like quasi_total Element of bool [:NAT,REAL:]

lim (P * P) is ext-real V43() V44() Element of REAL

Intersection P is V131() V132() V133() Element of bool REAL

P . (Intersection P) is set

dom (P * P) is V131() V132() V133() V134() V135() V136() Element of bool NAT

f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

(P * P) . f is ext-real V43() V44() Element of REAL

P . f is V131() V132() V133() Element of K105(REAL)

P . (P . f) is set

proj2 P is set

Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

P . Y is V131() V132() V133() Element of K105(REAL)

P . (P . Y) is set

(P * P) . Y is ext-real V43() V44() Element of REAL

f is ext-real V43() V44() Element of REAL

Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

(P * P) . Y is ext-real V43() V44() Element of REAL

Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

proj2 P is set

f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

P . f is V131() V132() V133() Element of K105(REAL)

f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

P . f is V131() V132() V133() Element of K105(REAL)

f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

P . f is V131() V132() V133() Element of K105(REAL)

Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

(P * P) . Y is ext-real V43() V44() Element of REAL

P . Y is V131() V132() V133() Element of K105(REAL)

P . (P . Y) is set

Y is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

(P * P) . Y is ext-real V43() V44() Element of REAL

f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

f is ext-real V36() V37() V38() V42() V43() V44() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

P . f is V131() V132() V133() Element of K105(REAL)

[:NAT,NAT:] is non empty Relation-like set

[:[:NAT,NAT:],(bool [:Borel_Sets,REAL:]):] is non empty Relation-like set

[0,0] is V1() Element of [:NAT,NAT:]

P is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[[0,0],P] is V1() Element of [:[:NAT,NAT:],(bool [:Borel_Sets,REAL:]):]

{[[0,0],P]} is non empty Relation-like [:NAT,NAT:] -defined bool [:Borel_Sets,REAL:] -valued Function-like Element of bool [:[:NAT,NAT:],(bool [:Borel_Sets,REAL:]):]

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

dom {[[0,0],P]} is non empty Relation-like NAT -defined NAT -valued Element of bool [:NAT,NAT:]

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

{[0,0]} is non empty Relation-like NAT -defined NAT -valued Function-like Element of bool [:NAT,NAT:]

[:{0},{0}:] is non empty Relation-like NAT -defined NAT -valued Element of bool [:NAT,NAT:]

proj2 {[[0,0],P]} is non empty set

{P} is non empty functional Element of bool (bool [:Borel_Sets,REAL:])

bool (bool [:Borel_Sets,REAL:]) is non empty V143() set

[:[:{0},{0}:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[:{0},{0}:],(REAL,Borel_Sets):] is non empty V143() set

Y is Relation-like [:{0},{0}:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[:{0},{0}:],(REAL,Borel_Sets):]

({0},{0},Y) is () ()

(({0},{0},Y)) is non empty set

the of ({0},{0},Y) is non empty set

(({0},{0},Y)) is non empty set

the of ({0},{0},Y) is non empty set

Q is Element of (({0},{0},Y))

x is Element of (({0},{0},Y))

Q is Element of (({0},{0},Y))

x is Element of (({0},{0},Y))

Q is Element of (({0},{0},Y))

x is Element of (({0},{0},Y))

p is ext-real V43() V44() Element of REAL

1 - p is ext-real V43() V44() Element of REAL

p is Element of (({0},{0},Y))

(({0},{0},Y),p,x) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of ({0},{0},Y) is Relation-like [: the of ({0},{0},Y), the of ({0},{0},Y):] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of ({0},{0},Y), the of ({0},{0},Y):],(REAL,Borel_Sets):]

[: the of ({0},{0},Y), the of ({0},{0},Y):] is non empty Relation-like set

[:[: the of ({0},{0},Y), the of ({0},{0},Y):],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of ({0},{0},Y), the of ({0},{0},Y):],(REAL,Borel_Sets):] is non empty V143() set

[p,x] is V1() Element of [:(({0},{0},Y)),(({0},{0},Y)):]

[:(({0},{0},Y)),(({0},{0},Y)):] is non empty Relation-like set

the of ({0},{0},Y) . [p,x] is set

(({0},{0},Y),p,Q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[p,Q] is V1() Element of [:(({0},{0},Y)),(({0},{0},Y)):]

the of ({0},{0},Y) . [p,Q] is set

q is Event of Borel_Sets

(({0},{0},Y),p,x) . q is ext-real V43() V44() Element of REAL

(({0},{0},Y),p,Q) . q is ext-real V43() V44() Element of REAL

p * ((({0},{0},Y),p,Q) . q) is ext-real V43() V44() Element of REAL

(1 - p) * ((({0},{0},Y),p,x) . q) is ext-real V43() V44() Element of REAL

(p * ((({0},{0},Y),p,Q) . q)) + ((1 - p) * ((({0},{0},Y),p,x) . q)) is ext-real V43() V44() Element of REAL

Q is set

[:Q,Q:] is Relation-like set

bool [:Q,Q:] is non empty V143() set

Q is () ()

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

Q is () ()

(Q) is set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

x is Element of (Q)

x `1 is set

x `2 is set

Q is () ()

(Q) is non empty set

the of Q is non empty set

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

x is Element of (Q)

p is Element of (Q)

(Q,p) is Event of Borel_Sets

(Q,p) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,p) is V131() V132() V133() set

(Q,p) is Element of (Q)

(Q,(Q,p),x) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]

[: the of Q, the of Q:] is non empty Relation-like set

[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set

[(Q,p),x] is V1() Element of [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

the of Q . [(Q,p),x] is set

(Q,(Q,p),x) . (Q,p) is ext-real V43() V44() Element of REAL

p is Event of Borel_Sets

(Q,(Q,p),x) . p is ext-real V43() V44() Element of REAL

1 - ((Q,(Q,p),x) . p) is ext-real V43() V44() Element of REAL

[#] Borel_Sets is Event of Borel_Sets

REAL \ p is V131() V132() V133() Element of bool REAL

p ` is V131() V132() V133() Element of bool REAL

REAL \ p is V131() V132() V133() set

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

x is Element of (Q)

(Q,x) is Element of (Q)

(Q,x) is Event of Borel_Sets

(Q,x) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,x) is V131() V132() V133() set

[(Q,x),((Q,x) `)] is V1() Element of [:(Q),(bool REAL):]

[:(Q),(bool REAL):] is non empty Relation-like set

p is Event of Borel_Sets

p is Element of (Q)

p is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Event of Borel_Sets

(Q,p) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,p) is V131() V132() V133() set

[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]

(Q,p) is Element of (Q)

(Q,p) is Event of Borel_Sets

(Q,p) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,p) is V131() V132() V133() set

[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]

((Q,p) `) ` is V131() V132() V133() Element of bool REAL

REAL \ ((Q,p) `) is V131() V132() V133() set

[(Q,p),(((Q,p) `) `)] is V1() Element of [:(Q),(bool REAL):]

[(Q,p),(((Q,p) `) `)] is V1() Element of [:(Q),(bool REAL):]

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

(Q) is non empty set

the of Q is non empty set

p is Element of (Q)

(Q,p) is Element of (Q)

q is Element of (Q)

(Q,(Q,p),q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]

[: the of Q, the of Q:] is non empty Relation-like set

[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set

[(Q,p),q] is V1() Element of [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

the of Q . [(Q,p),q] is set

(Q,p) is Event of Borel_Sets

(Q,(Q,p),q) . (Q,p) is ext-real V43() V44() Element of REAL

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

p is Element of (Q)

q is Element of (Q)

p is Element of (Q)

q is Element of (Q)

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

(Q) is non empty set

the of Q is non empty set

x is Element of (Q)

(Q,x) is Element of (Q)

(Q,x) is Event of Borel_Sets

p is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Event of Borel_Sets

p is Element of (Q)

(Q,(Q,x),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]

[: the of Q, the of Q:] is non empty Relation-like set

[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set

[(Q,x),p] is V1() Element of [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

the of Q . [(Q,x),p] is set

(Q,(Q,x),p) . (Q,x) is ext-real V43() V44() Element of REAL

(Q,(Q,p),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,p),p] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,p),p] is set

(Q,(Q,p),p) . (Q,p) is ext-real V43() V44() Element of REAL

p is Element of (Q)

(Q,(Q,x),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]

[: the of Q, the of Q:] is non empty Relation-like set

[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set

[(Q,x),p] is V1() Element of [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

the of Q . [(Q,x),p] is set

(Q,(Q,x),p) . (Q,x) is ext-real V43() V44() Element of REAL

(Q,(Q,p),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,p),p] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,p),p] is set

(Q,(Q,p),p) . (Q,p) is ext-real V43() V44() Element of REAL

p is Element of (Q)

(Q,(Q,p),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]

[: the of Q, the of Q:] is non empty Relation-like set

[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set

[(Q,p),p] is V1() Element of [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

the of Q . [(Q,p),p] is set

(Q,(Q,p),p) . (Q,p) is ext-real V43() V44() Element of REAL

(Q,(Q,x),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,x),p] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,x),p] is set

(Q,(Q,x),p) . (Q,x) is ext-real V43() V44() Element of REAL

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

x is Element of (Q)

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

x is Element of (Q)

p is Element of (Q)

p is Element of (Q)

(Q) is non empty set

the of Q is non empty set

(Q,x) is Element of (Q)

q is Element of (Q)

(Q,(Q,x),q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]

[: the of Q, the of Q:] is non empty Relation-like set

[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set

[(Q,x),q] is V1() Element of [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

the of Q . [(Q,x),q] is set

(Q,x) is Event of Borel_Sets

(Q,(Q,x),q) . (Q,x) is ext-real V43() V44() Element of REAL

(Q,p) is Element of (Q)

(Q,(Q,p),q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,p),q] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,p),q] is set

(Q,p) is Event of Borel_Sets

(Q,(Q,p),q) . (Q,p) is ext-real V43() V44() Element of REAL

(Q,p) is Element of (Q)

(Q,(Q,p),q) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,p),q] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,p),q] is set

(Q,p) is Event of Borel_Sets

(Q,(Q,p),q) . (Q,p) is ext-real V43() V44() Element of REAL

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

x is Element of (Q)

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

x is Element of (Q)

p is Element of (Q)

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

x is Element of (Q)

p is Element of (Q)

p is Element of (Q)

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

x is Element of (Q)

(Q,x) is Element of (Q)

(Q,x) is Element of (Q)

(Q,x) is Event of Borel_Sets

(Q,x) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,x) is V131() V132() V133() set

[(Q,x),((Q,x) `)] is V1() Element of [:(Q),(bool REAL):]

[:(Q),(bool REAL):] is non empty Relation-like set

p is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Event of Borel_Sets

(Q,p) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,p) is V131() V132() V133() set

[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]

(Q) is non empty set

the of Q is non empty set

(Q,(Q,p)) is Element of (Q)

p is Element of (Q)

(Q,(Q,(Q,p)),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]

[: the of Q, the of Q:] is non empty Relation-like set

[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set

[(Q,(Q,p)),p] is V1() Element of [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

the of Q . [(Q,(Q,p)),p] is set

(Q,(Q,p)) is Event of Borel_Sets

(Q,(Q,(Q,p)),p) . (Q,(Q,p)) is ext-real V43() V44() Element of REAL

(Q,(Q,x)) is Element of (Q)

(Q,(Q,(Q,x)),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,(Q,x)),p] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,(Q,x)),p] is set

(Q,(Q,x)) is Event of Borel_Sets

(Q,(Q,(Q,x)),p) . (Q,(Q,x)) is ext-real V43() V44() Element of REAL

(Q,(Q,x),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,x),p] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,x),p] is set

r is Event of Borel_Sets

(Q,(Q,x),p) . r is ext-real V43() V44() Element of REAL

(Q,(Q,p),p) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,p),p] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,p),p] is set

q is Event of Borel_Sets

(Q,(Q,p),p) . q is ext-real V43() V44() Element of REAL

1 - ((Q,(Q,x),p) . r) is ext-real V43() V44() Element of REAL

- (1 - ((Q,(Q,x),p) . r)) is ext-real V43() V44() Element of REAL

((Q,(Q,x),p) . r) - 1 is ext-real V43() V44() Element of REAL

1 - ((Q,(Q,p),p) . q) is ext-real V43() V44() Element of REAL

- (1 - ((Q,(Q,p),p) . q)) is ext-real V43() V44() Element of REAL

((Q,(Q,p),p) . q) - 1 is ext-real V43() V44() Element of REAL

(Q,(Q,p),p) . (Q,p) is ext-real V43() V44() Element of REAL

(Q,(Q,x),p) . (Q,x) is ext-real V43() V44() Element of REAL

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

[:(Q),(Q):] is non empty Relation-like set

bool [:(Q),(Q):] is non empty V143() set

p is Element of (Q)

x is set

q is Element of (Q)

p is set

q is Element of (Q)

x is set

r is Element of (Q)

p is set

q is Element of (Q)

E is Element of (Q)

p is set

x is set

x is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

p is Element of (Q)

p is Element of (Q)

[p,p] is V1() Element of [:(Q),(Q):]

q is Element of (Q)

r is Element of (Q)

p is Element of (Q)

p is Element of (Q)

[p,p] is V1() Element of [:(Q),(Q):]

q is Element of (Q)

r is Element of (Q)

[q,r] is V1() Element of [:(Q),(Q):]

x is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

p is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

p is Element of (Q)

q is Element of (Q)

[p,q] is V1() Element of [:(Q),(Q):]

p is set

q is set

[p,q] is V1() set

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

bool (Q) is non empty V143() set

(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

bool [:(Q),(Q):] is non empty V143() set

Class (Q) is non empty V20() a_partition of (Q)

x is Element of bool (Q)

p is Element of bool (Q)

p is Element of (Q)

q is Element of (Q)

r is Element of (Q)

q is Element of (Q)

(Q) is non empty set

the of Q is non empty set

(Q,q) is Element of (Q)

E is Element of (Q)

(Q,(Q,q),E) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]

[: the of Q, the of Q:] is non empty Relation-like set

[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set

[(Q,q),E] is V1() Element of [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

the of Q . [(Q,q),E] is set

(Q,q) is Event of Borel_Sets

(Q,(Q,q),E) . (Q,q) is ext-real V43() V44() Element of REAL

(Q,q) is Element of (Q)

(Q,(Q,q),E) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,q),E] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,q),E] is set

(Q,q) is Event of Borel_Sets

(Q,(Q,q),E) . (Q,q) is ext-real V43() V44() Element of REAL

[r,q] is V1() Element of [:(Q),(Q):]

s is set

Class ((Q),s) is Element of bool (Q)

(Q,r) is Element of (Q)

(Q,(Q,r),E) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,r),E] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,r),E] is set

(Q,r) is Event of Borel_Sets

(Q,(Q,r),E) . (Q,r) is ext-real V43() V44() Element of REAL

[p,q] is V1() Element of [:(Q),(Q):]

s is set

Class ((Q),s) is Element of bool (Q)

(Q,p) is Element of (Q)

(Q,(Q,p),E) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,p),E] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,p),E] is set

(Q,p) is Event of Borel_Sets

(Q,(Q,p),E) . (Q,p) is ext-real V43() V44() Element of REAL

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

bool [:(Q),(Q):] is non empty V143() set

Class (Q) is non empty V20() a_partition of (Q)

[:(Class (Q)),(Class (Q)):] is non empty Relation-like set

bool [:(Class (Q)),(Class (Q)):] is non empty V143() set

bool (Q) is non empty V143() set

x is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]

p is Element of bool (Q)

p is Element of bool (Q)

[p,p] is V1() Element of [:(bool (Q)),(bool (Q)):]

[:(bool (Q)),(bool (Q)):] is non empty Relation-like set

q is Element of (Q)

r is Element of (Q)

q is Element of bool (Q)

E is Element of bool (Q)

x is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]

p is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]

p is Element of bool (Q)

q is Element of bool (Q)

[p,q] is V1() Element of [:(bool (Q)),(bool (Q)):]

[:(bool (Q)),(bool (Q)):] is non empty Relation-like set

r is Element of (Q)

q is Element of (Q)

r is Element of (Q)

q is Element of (Q)

p is set

q is set

[p,q] is V1() set

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

bool (Q) is non empty V143() set

(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

bool [:(Q),(Q):] is non empty V143() set

(Q) is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]

Class (Q) is non empty V20() a_partition of (Q)

[:(Class (Q)),(Class (Q)):] is non empty Relation-like set

bool [:(Class (Q)),(Class (Q)):] is non empty V143() set

x is Element of (Q)

Class ((Q),x) is Element of bool (Q)

p is Element of (Q)

Class ((Q),p) is Element of bool (Q)

[(Class ((Q),x)),(Class ((Q),p))] is V1() Element of [:(bool (Q)),(bool (Q)):]

[:(bool (Q)),(bool (Q)):] is non empty Relation-like set

[x,x] is V1() Element of [:(Q),(Q):]

[p,p] is V1() Element of [:(Q),(Q):]

p is Element of (Q)

q is Element of (Q)

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

bool (Q) is non empty V143() set

(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

bool [:(Q),(Q):] is non empty V143() set

Class (Q) is non empty V20() a_partition of (Q)

x is Element of bool (Q)

p is Element of bool (Q)

p is set

Class ((Q),p) is Element of bool (Q)

q is Element of (Q)

(Q,q) is Element of (Q)

(Q,q) is Element of (Q)

(Q,q) is Event of Borel_Sets

(Q,q) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,q) is V131() V132() V133() set

[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]

[:(Q),(bool REAL):] is non empty Relation-like set

r is Element of (Q)

(Q,r) is Element of (Q)

(Q,r) is Element of (Q)

(Q,r) is Event of Borel_Sets

(Q,r) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,r) is V131() V132() V133() set

[(Q,r),((Q,r) `)] is V1() Element of [:(Q),(bool REAL):]

[q,r] is V1() Element of [:(Q),(Q):]

q is set

Class ((Q),q) is Element of bool (Q)

(Q) is non empty set

the of Q is non empty set

s is Element of (Q)

(Q,(Q,q),s) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

the of Q is Relation-like [: the of Q, the of Q:] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):]

[: the of Q, the of Q:] is non empty Relation-like set

[:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty Relation-like set

bool [:[: the of Q, the of Q:],(REAL,Borel_Sets):] is non empty V143() set

[(Q,q),s] is V1() Element of [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

the of Q . [(Q,q),s] is set

E is Event of Borel_Sets

(Q,(Q,q),s) . E is ext-real V43() V44() Element of REAL

(Q,(Q,r),s) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,r),s] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,r),s] is set

q is Event of Borel_Sets

(Q,(Q,r),s) . q is ext-real V43() V44() Element of REAL

(Q,(Q,q)) is Element of (Q)

(Q,(Q,q)) is Event of Borel_Sets

(Q,(Q,r)) is Element of (Q)

1 - ((Q,(Q,q),s) . E) is ext-real V43() V44() Element of REAL

(Q,(Q,q),s) . (Q,q) is ext-real V43() V44() Element of REAL

(Q,(Q,r),s) . (Q,r) is ext-real V43() V44() Element of REAL

1 - ((Q,(Q,r),s) . q) is ext-real V43() V44() Element of REAL

(Q,(Q,(Q,q)),s) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,(Q,q)),s] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,(Q,q)),s] is set

(Q,(Q,(Q,q)),s) . (Q,(Q,q)) is ext-real V43() V44() Element of REAL

(Q,(Q,(Q,r)),s) is Relation-like Borel_Sets -defined REAL -valued Function-like quasi_total V54() Probability of Borel_Sets

[(Q,(Q,r)),s] is V1() Element of [:(Q),(Q):]

the of Q . [(Q,(Q,r)),s] is set

(Q,(Q,r)) is Event of Borel_Sets

(Q,(Q,(Q,r)),s) . (Q,(Q,r)) is ext-real V43() V44() Element of REAL

q is Element of (Q)

[(Q,q),q] is V1() Element of [:(Q),(Q):]

[(Q,r),q] is V1() Element of [:(Q),(Q):]

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

bool (Q) is non empty V143() set

(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

bool [:(Q),(Q):] is non empty V143() set

Class (Q) is non empty V20() a_partition of (Q)

x is Element of bool (Q)

p is Element of bool (Q)

p is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Event of Borel_Sets

(Q,p) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,p) is V131() V132() V133() set

[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]

[:(Q),(bool REAL):] is non empty Relation-like set

q is Element of (Q)

(Q,q) is Element of (Q)

(Q,q) is Element of (Q)

(Q,q) is Event of Borel_Sets

(Q,q) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,q) is V131() V132() V133() set

[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]

(Q,(Q,p)) is Element of (Q)

(Q,(Q,p)) is Element of (Q)

(Q,(Q,p)) is Event of Borel_Sets

(Q,(Q,p)) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,(Q,p)) is V131() V132() V133() set

[(Q,(Q,p)),((Q,(Q,p)) `)] is V1() Element of [:(Q),(bool REAL):]

(Q,(Q,q)) is Element of (Q)

(Q,(Q,q)) is Element of (Q)

(Q,(Q,q)) is Event of Borel_Sets

(Q,(Q,q)) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,(Q,q)) is V131() V132() V133() set

[(Q,(Q,q)),((Q,(Q,q)) `)] is V1() Element of [:(Q),(bool REAL):]

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

bool [:(Q),(Q):] is non empty V143() set

Class (Q) is non empty V20() a_partition of (Q)

[:(Class (Q)),(Class (Q)):] is non empty Relation-like set

bool [:(Class (Q)),(Class (Q)):] is non empty V143() set

x is set

p is Element of (Q)

Class ((Q),p) is Element of bool (Q)

bool (Q) is non empty V143() set

(Q,p) is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Event of Borel_Sets

(Q,p) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,p) is V131() V132() V133() set

[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]

[:(Q),(bool REAL):] is non empty Relation-like set

Class ((Q),(Q,p)) is Element of bool (Q)

p is set

q is Element of (Q)

Class ((Q),q) is Element of bool (Q)

(Q,q) is Element of (Q)

(Q,q) is Element of (Q)

(Q,q) is Event of Borel_Sets

(Q,q) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,q) is V131() V132() V133() set

[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]

Class ((Q),(Q,q)) is Element of bool (Q)

r is Element of bool (Q)

q is Element of bool (Q)

x is Relation-like Class (Q) -defined Class (Q) -valued Function-like quasi_total Element of bool [:(Class (Q)),(Class (Q)):]

p is Element of (Q)

Class ((Q),p) is Element of bool (Q)

bool (Q) is non empty V143() set

x . (Class ((Q),p)) is set

(Q,p) is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Event of Borel_Sets

(Q,p) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,p) is V131() V132() V133() set

[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]

[:(Q),(bool REAL):] is non empty Relation-like set

Class ((Q),(Q,p)) is Element of bool (Q)

x is Relation-like Class (Q) -defined Class (Q) -valued Function-like quasi_total Element of bool [:(Class (Q)),(Class (Q)):]

p is Relation-like Class (Q) -defined Class (Q) -valued Function-like quasi_total Element of bool [:(Class (Q)),(Class (Q)):]

p is set

q is Element of (Q)

Class ((Q),q) is Element of bool (Q)

bool (Q) is non empty V143() set

x . p is set

(Q,q) is Element of (Q)

(Q,q) is Element of (Q)

(Q,q) is Event of Borel_Sets

(Q,q) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,q) is V131() V132() V133() set

[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]

[:(Q),(bool REAL):] is non empty Relation-like set

Class ((Q),(Q,q)) is Element of bool (Q)

p . p is set

Q is () ()

(Q) is non empty set

(Q) is non empty set

the of Q is non empty set

[:(Q),Borel_Sets:] is non empty Relation-like set

(Q) is Relation-like (Q) -defined (Q) -valued reflexive symmetric transitive V31((Q)) Element of bool [:(Q),(Q):]

[:(Q),(Q):] is non empty Relation-like set

bool [:(Q),(Q):] is non empty V143() set

Class (Q) is non empty V20() a_partition of (Q)

(Q) is Relation-like Class (Q) -defined Class (Q) -valued Element of bool [:(Class (Q)),(Class (Q)):]

[:(Class (Q)),(Class (Q)):] is non empty Relation-like set

bool [:(Class (Q)),(Class (Q)):] is non empty V143() set

(Q) is Relation-like Class (Q) -defined Class (Q) -valued Function-like quasi_total Element of bool [:(Class (Q)),(Class (Q)):]

((Class (Q)),(Q),(Q)) is () ()

x is set

p is set

[x,p] is V1() set

p is set

[p,p] is V1() set

[x,p] is V1() set

q is Element of (Q)

Class ((Q),q) is Element of bool (Q)

bool (Q) is non empty V143() set

r is Element of (Q)

Class ((Q),r) is Element of bool (Q)

q is Element of (Q)

Class ((Q),q) is Element of bool (Q)

x is set

p is set

[x,p] is V1() set

[p,x] is V1() set

p is Element of (Q)

Class ((Q),p) is Element of bool (Q)

bool (Q) is non empty V143() set

q is Element of (Q)

Class ((Q),q) is Element of bool (Q)

[p,q] is V1() Element of [:(Q),(Q):]

bool (Q) is non empty V143() set

x is Element of Class (Q)

p is Element of Class (Q)

[x,p] is V1() Element of [:(Class (Q)),(Class (Q)):]

(Q) . p is Element of Class (Q)

(Q) . x is Element of Class (Q)

[((Q) . p),((Q) . x)] is V1() Element of [:(Class (Q)),(Class (Q)):]

p is Element of (Q)

Class ((Q),p) is Element of bool (Q)

q is Element of (Q)

Class ((Q),q) is Element of bool (Q)

(Q,q) is Element of (Q)

(Q,q) is Element of (Q)

(Q,q) is Event of Borel_Sets

(Q,q) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,q) is V131() V132() V133() set

[(Q,q),((Q,q) `)] is V1() Element of [:(Q),(bool REAL):]

[:(Q),(bool REAL):] is non empty Relation-like set

(Q,p) is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Event of Borel_Sets

(Q,p) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,p) is V131() V132() V133() set

[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]

(Q) . (Class ((Q),p)) is set

Class ((Q),(Q,p)) is Element of bool (Q)

(Q) . (Class ((Q),q)) is set

Class ((Q),(Q,q)) is Element of bool (Q)

x is Element of Class (Q)

(Q) . x is set

(Q) . ((Q) . x) is set

p is Element of (Q)

Class ((Q),p) is Element of bool (Q)

(Q) . x is Element of Class (Q)

(Q) . ((Q) . x) is Element of Class (Q)

(Q,p) is Element of (Q)

(Q,p) is Element of (Q)

(Q,p) is Event of Borel_Sets

(Q,p) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,p) is V131() V132() V133() set

[(Q,p),((Q,p) `)] is V1() Element of [:(Q),(bool REAL):]

[:(Q),(bool REAL):] is non empty Relation-like set

Class ((Q),(Q,p)) is Element of bool (Q)

(Q) . (Class ((Q),(Q,p))) is set

(Q,(Q,p)) is Element of (Q)

(Q,(Q,p)) is Element of (Q)

(Q,(Q,p)) is Event of Borel_Sets

(Q,(Q,p)) ` is V131() V132() V133() Element of bool REAL

REAL \ (Q,(Q,p)) is V131() V132() V133() set

[(Q,(Q,p)),((Q,(Q,p)) `)] is V1() Element of [:(Q),(bool REAL):]

Class ((Q),(Q,(Q,p))) is Element of bool (Q)

x is set

[x,x] is V1() set

p is Element of (Q)

Class ((Q),p) is Element of bool (Q)