:: 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
is non empty Relation-like set
bool is non empty V143() set
bool () 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

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

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

(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 ()
is non empty Relation-like set
bool 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)
is non empty functional V131() V132() V133() V134() V135() V136() Element of bool NAT
bool NAT is non empty V143() set

bool is non empty V143() set

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

lim (P * P) is ext-real V43() V44() Element of REAL
Intersection P is V131() V132() V133() Element of bool REAL
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)
is non empty Relation-like set

[0,0] is V1() Element of

[[0,0],P] is V1() Element of

bool is non empty V143() set

bool is non empty V143() set

proj2 {[[0,0],P]} is non empty set
{P} is non empty functional Element of bool
bool is non empty V143() set
is non empty Relation-like set
bool is non empty V143() set

(,,Y) is () ()
((,,Y)) is non empty set
the of (,,Y) is non empty set
((,,Y)) is non empty set
the of (,,Y) is non empty set
Q is Element of ((,,Y))
x is Element of ((,,Y))
Q is Element of ((,,Y))
x is Element of ((,,Y))
Q is Element of ((,,Y))
x is Element of ((,,Y))
p is ext-real V43() V44() Element of REAL
1 - p is ext-real V43() V44() Element of REAL
p is Element of ((,,Y))

the of (,,Y) is Relation-like [: the of (,,Y), the of (,,Y):] -defined (REAL,Borel_Sets) -valued Function-like quasi_total Element of bool [:[: the of (,,Y), the of (,,Y):],(REAL,Borel_Sets):]
[: the of (,,Y), the of (,,Y):] is non empty Relation-like set
[:[: the of (,,Y), the of (,,Y):],(REAL,Borel_Sets):] is non empty Relation-like set
bool [:[: the of (,,Y), the of (,,Y):],(REAL,Borel_Sets):] is non empty V143() set
[p,x] is V1() Element of [:((,,Y)),((,,Y)):]
[:((,,Y)),((,,Y)):] is non empty Relation-like set
the of (,,Y) . [p,x] is set

[p,Q] is V1() Element of [:((,,Y)),((,,Y)):]
the of (,,Y) . [p,Q] is set
q is Event of Borel_Sets
((,,Y),p,x) . q is ext-real V43() V44() Element of REAL
((,,Y),p,Q) . q is ext-real V43() V44() Element of REAL
p * (((,,Y),p,Q) . q) is ext-real V43() V44() Element of REAL
(1 - p) * (((,,Y),p,x) . q) is ext-real V43() V44() Element of REAL
(p * (((,,Y),p,Q) . q)) + ((1 - p) * (((,,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)

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

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),():]
[:(Q),():] 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),():]
(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),():]
((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),():]
[(Q,p),(((Q,p) `) `)] is V1() 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
p is Element of (Q)
(Q,p) is Element of (Q)
q is Element of (Q)

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)

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,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)

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,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)

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,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)

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,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,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),():]
[:(Q),():] 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),():]
(Q) is non empty set
the of Q is non empty set
(Q,(Q,p)) is Element of (Q)
p is Element of (Q)

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,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,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,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)

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),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,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,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),():]
[:(Q),():] 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),():]
[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)

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,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)),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,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),():]
[:(Q),():] 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),():]
(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),():]
(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),():]
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),():]
[:(Q),():] 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),():]
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),():]
[:(Q),():] 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),():]
[:(Q),():] 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),():]
[:(Q),():] 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),():]
(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),():]
[:(Q),():] 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),():]
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)