:: KOLMOG01 semantic presentation

REAL is non empty non trivial non finite V79() V80() V81() V85() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() Element of bool REAL
bool REAL is non empty cup-closed intersection_stable diff-closed preBoolean set
ExtREAL is non empty V80() set
[:NAT,ExtREAL:] is non empty Relation-like V34() set
bool [:NAT,ExtREAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
bool ExtREAL is non empty cup-closed intersection_stable diff-closed preBoolean set
omega is non empty epsilon-transitive epsilon-connected ordinal V79() V80() V81() V82() V83() V84() V85() set
bool omega is non empty cup-closed intersection_stable diff-closed preBoolean set
[:NAT,REAL:] is non empty Relation-like V33() V34() V35() set
bool [:NAT,REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool REAL) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool NAT is non empty cup-closed intersection_stable diff-closed preBoolean set
COMPLEX is non empty non trivial non finite V79() V85() set
RAT is non empty non trivial non finite V79() V80() V81() V82() V85() set
INT is non empty non trivial non finite V79() V80() V81() V82() V83() V85() set
[:COMPLEX,COMPLEX:] is non empty Relation-like V33() set
bool [:COMPLEX,COMPLEX:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty Relation-like V33() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:REAL,REAL:] is non empty Relation-like V33() V34() V35() set
bool [:REAL,REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:[:REAL,REAL:],REAL:] is non empty Relation-like V33() V34() V35() set
bool [:[:REAL,REAL:],REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:RAT,RAT:] is non empty Relation-like RAT -valued V33() V34() V35() set
bool [:RAT,RAT:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:[:RAT,RAT:],RAT:] is non empty Relation-like RAT -valued V33() V34() V35() set
bool [:[:RAT,RAT:],RAT:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:INT,INT:] is non empty Relation-like RAT -valued INT -valued V33() V34() V35() set
bool [:INT,INT:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:[:INT,INT:],INT:] is non empty Relation-like RAT -valued INT -valued V33() V34() V35() set
bool [:[:INT,INT:],INT:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:NAT,NAT:] is non empty Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
[:[:NAT,NAT:],NAT:] is non empty Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
bool [:[:NAT,NAT:],NAT:] is non empty cup-closed intersection_stable diff-closed preBoolean set
1 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
2 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
3 is ext-real non empty epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
0 is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V77() V78() V79() V80() V81() V82() V83() V84() V85() Element of NAT
the ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() set is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() set
{} is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() set
union {} is epsilon-transitive epsilon-connected ordinal finite set
Omega is Relation-like Function-like set
dom Omega is set
I is set
Omega | I is Relation-like Function-like set
rng (Omega | I) is set
the Element of I is Element of I
Omega is ext-real V14() real Element of REAL
Omega * Omega is ext-real V14() real set
Omega - 1 is ext-real V14() real set
Omega * (Omega - 1) is ext-real V14() real set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
{{},Omega} is non empty finite intersection_stable set
I is Element of bool (bool Omega)
sigma I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool Omega is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty Relation-like set
bool [:NAT,(bool Omega):] is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty Relation-like NAT -defined bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng Sigma is non empty Element of bool (bool Omega)
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
Union Sigma is Element of bool Omega
rng Sigma is non empty set
union (rng Sigma) is set
Partial_Union Sigma is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union Sigma) . P is Event of bool Omega
a is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
(Partial_Union Sigma) . a is set
a + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union Sigma) . (a + 1) is set
F is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
F + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
Sigma . (F + 1) is Event of bool Omega
(Partial_Union Sigma) . (F + 1) is Event of bool Omega
{} \/ (Sigma . (F + 1)) is set
(Partial_Union Sigma) . (F + 1) is Event of bool Omega
Omega \/ (Sigma . (F + 1)) is non empty set
(Partial_Union Sigma) . (F + 1) is Event of bool Omega
{} \/ (Sigma . (F + 1)) is set
Omega \/ (Sigma . (F + 1)) is non empty set
(Partial_Union Sigma) . 0 is Event of bool Omega
Sigma . 0 is Event of bool Omega
(Partial_Union Sigma) . 0 is set
Union (Partial_Union Sigma) is Element of bool Omega
rng (Partial_Union Sigma) is non empty set
union (rng (Partial_Union Sigma)) is set
P is set
a is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union Sigma) . a is Event of bool Omega
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union Sigma) . P is Event of bool Omega
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union Sigma) . P is Event of bool Omega
a is set
P is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union Sigma) . P is Event of bool Omega
Sigma is Element of bool Omega
Sigma ` is Element of bool Omega
Omega \ Sigma is set
Sigma is set
Sigma is set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is Element of bool I
P is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
a is set
F is set
F is Element of bool I
T is Element of I
P . T is ext-real V14() real Element of REAL
Ie is Element of Sigma
T /\ Ie is Element of bool Omega
P . (T /\ Ie) is ext-real V14() real set
P . Ie is ext-real V14() real set
(P . T) * (P . Ie) is ext-real V14() real set
a is Element of bool I
F is Element of bool I
T is Element of I
P . T is ext-real V14() real Element of REAL
Ie is Element of Sigma
T /\ Ie is Element of bool Omega
P . (T /\ Ie) is ext-real V14() real set
P . Ie is ext-real V14() real set
(P . T) * (P . Ie) is ext-real V14() real set
Ie is Element of Sigma
T /\ Ie is Element of bool Omega
P . (T /\ Ie) is ext-real V14() real set
P . Ie is ext-real V14() real set
(P . T) * (P . Ie) is ext-real V14() real set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty Relation-like set
bool [:NAT,(bool Omega):] is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
a is Element of P
Sigma . a is ext-real V14() real Element of REAL
F is non empty Relation-like NAT -defined bool Omega -valued I -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Union F is Element of bool Omega
rng F is non empty set
union (rng F) is set
a /\ (Union F) is Element of bool Omega
Sigma . (a /\ (Union F)) is ext-real V14() real set
Sigma . (Union F) is ext-real V14() real set
(Sigma . a) * (Sigma . (Union F)) is ext-real V14() real set
T is Element of I
Sigma . T is ext-real V14() real Element of REAL
seqIntersection (T,F) is non empty Relation-like NAT -defined bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
u is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(seqIntersection (T,F)) . u is Event of bool Omega
F . u is Event of I
T /\ (F . u) is Event of I
Partial_Union F is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
seqIntersection (T,(Partial_Union F)) is non empty Relation-like NAT -defined bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
v is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(seqIntersection (T,(Partial_Union F))) . v is Event of bool Omega
(Partial_Union F) . v is Event of I
T /\ ((Partial_Union F) . v) is Event of I
T /\ (Union F) is Element of bool Omega
Union (Partial_Union F) is Element of bool Omega
rng (Partial_Union F) is non empty set
union (rng (Partial_Union F)) is set
T /\ (Union (Partial_Union F)) is Element of bool Omega
v is non empty Relation-like NAT -defined bool Omega -valued I -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Union v is Element of bool Omega
rng v is non empty set
union (rng v) is set
u is non empty Relation-like NAT -defined bool Omega -valued I -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Sigma * u is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
x is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Sigma * u) . x is ext-real V14() real Element of REAL
u . x is Event of I
Sigma . (u . x) is ext-real V14() real Element of REAL
F . x is Event of I
(F . x) /\ T is Event of I
Sigma . ((F . x) /\ T) is ext-real V14() real Element of REAL
Sigma . (F . x) is ext-real V14() real Element of REAL
(Sigma . (F . x)) * (Sigma . T) is ext-real V14() real set
Sigma * F is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Sigma * F) . x is ext-real V14() real Element of REAL
Ie is ext-real V14() real set
((Sigma * F) . x) * Ie is ext-real V14() real set
Ie (#) (Sigma * F) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
(Ie (#) (Sigma * F)) . x is ext-real V14() real Element of REAL
x is set
y is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union F) . y is Event of I
E1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union F) . E1 is Event of I
E is non empty Relation-like NAT -defined bool Omega -valued I -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
E . y is Event of I
E . E1 is Event of I
x is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(seqIntersection (T,(Partial_Union F))) . x is Event of bool Omega
E is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(seqIntersection (T,(Partial_Union F))) . E is Event of bool Omega
y is set
(Partial_Union F) . x is Event of I
T /\ ((Partial_Union F) . x) is Event of I
(Partial_Union F) . E is Event of I
T /\ ((Partial_Union F) . E) is Event of I
Partial_Union u is non empty Relation-like NAT -defined bool Omega -valued bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
x is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union u) . x is Event of I
(seqIntersection (T,(Partial_Union F))) . x is Event of bool Omega
E is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
(Partial_Union u) . E is set
(seqIntersection (T,(Partial_Union F))) . E is set
E + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union u) . (E + 1) is set
(seqIntersection (T,(Partial_Union F))) . (E + 1) is set
y is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
(Partial_Union u) . (y + 1) is Event of I
(Partial_Union u) . y is Event of I
u . (y + 1) is Event of I
((Partial_Union u) . y) \/ (u . (y + 1)) is Event of I
(Partial_Union F) . y is Event of I
T /\ ((Partial_Union F) . y) is Event of I
(T /\ ((Partial_Union F) . y)) \/ (u . (y + 1)) is Event of I
F . (y + 1) is Event of I
T /\ (F . (y + 1)) is Event of I
(T /\ ((Partial_Union F) . y)) \/ (T /\ (F . (y + 1))) is Event of I
((Partial_Union F) . y) \/ (F . (y + 1)) is Event of I
T /\ (((Partial_Union F) . y) \/ (F . (y + 1))) is Event of I
(Partial_Union F) . (y + 1) is Event of I
T /\ ((Partial_Union F) . (y + 1)) is Event of I
(seqIntersection (T,(Partial_Union F))) . (y + 1) is Event of bool Omega
(Partial_Union u) . 0 is Event of I
u . 0 is Event of I
F . 0 is Event of I
T /\ (F . 0) is Event of I
(Partial_Union F) . 0 is Event of I
T /\ ((Partial_Union F) . 0) is Event of I
(seqIntersection (T,(Partial_Union F))) . 0 is Event of bool Omega
(Partial_Union u) . 0 is set
(seqIntersection (T,(Partial_Union F))) . 0 is set
Sigma * (seqIntersection (T,(Partial_Union F))) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() Element of bool [:NAT,REAL:]
Sigma * (Partial_Union u) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (Sigma * u) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Partial_Sums (Sigma * F) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Ie (#) (Partial_Sums (Sigma * F)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Sigma * (Partial_Union F) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
Ie (#) (Sigma * (Partial_Union F)) is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim (Sigma * (Partial_Union F)) is ext-real V14() real Element of REAL
Ie * (lim (Sigma * (Partial_Union F))) is ext-real V14() real set
Sigma * v is non empty Relation-like NAT -defined REAL -valued Function-like V26( NAT ) V30( NAT , REAL ) V33() V34() V35() Element of bool [:NAT,REAL:]
lim (Sigma * v) is ext-real V14() real Element of REAL
Sigma . (T /\ (Union F)) is ext-real V14() real set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
(Omega,I,P,Sigma) is Element of bool I
Sigma . {} is ext-real V14() real set
a is Element of P
{} /\ a is Relation-like finite V79() V80() V81() V82() V83() V84() set
Sigma . ({} /\ a) is ext-real V14() real set
Sigma . a is ext-real V14() real Element of REAL
(Sigma . {}) * (Sigma . a) is ext-real V14() real set
F is Event of I
{} /\ F is Relation-like finite V79() V80() V81() V82() V83() V84() Element of bool Omega
Sigma . ({} /\ F) is ext-real V14() real set
bool Omega is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Omega)
[:NAT,(bool Omega):] is non empty Relation-like set
bool [:NAT,(bool Omega):] is non empty cup-closed intersection_stable diff-closed preBoolean set
F is non empty Relation-like NAT -defined bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
rng F is non empty Element of bool (bool Omega)
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
Union F is Element of bool Omega
rng F is non empty set
union (rng F) is set
T is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
F . T is Event of bool Omega
dom F is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
dom F is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
dom F is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
T is non empty Relation-like NAT -defined I -valued bool Omega -valued Function-like V26( NAT ) V30( NAT , bool Omega) Element of bool [:NAT,(bool Omega):]
Union T is Element of bool Omega
rng T is non empty set
union (rng T) is set
u is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
T . u is Event of I
Sigma . (T . u) is ext-real V14() real Element of REAL
v is Element of P
(T . u) /\ v is Event of I
Sigma . ((T . u) /\ v) is ext-real V14() real Element of REAL
Sigma . v is ext-real V14() real Element of REAL
(Sigma . (T . u)) * (Sigma . v) is ext-real V14() real set
dom T is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
rng T is non empty Element of bool I
dom T is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
dom T is non empty V79() V80() V81() V82() V83() V84() Element of bool NAT
Ie is Element of I
Sigma . Ie is ext-real V14() real Element of REAL
u is Element of P
Ie /\ u is Event of I
Sigma . (Ie /\ u) is ext-real V14() real Element of REAL
Sigma . u is ext-real V14() real Element of REAL
(Sigma . Ie) * (Sigma . u) is ext-real V14() real set
F is Element of bool Omega
F ` is Element of bool Omega
Omega \ F is set
T is Event of I
T ` is Element of bool Omega
Omega \ T is set
Sigma . (T `) is ext-real V14() real set
u is Element of P
(T `) /\ u is Element of bool Omega
Sigma . ((T `) /\ u) is ext-real V14() real set
Sigma . u is ext-real V14() real Element of REAL
(Sigma . (T `)) * (Sigma . u) is ext-real V14() real set
u /\ T is Event of I
Sigma . (u /\ T) is ext-real V14() real Element of REAL
Sigma . T is ext-real V14() real Element of REAL
(Sigma . u) * (Sigma . T) is ext-real V14() real set
[#] I is Event of I
([#] I) \ T is Event of I
Ie is Element of I
a is Element of bool (bool Omega)
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
(Omega,I,P,Sigma) is Element of bool I
F is Element of bool (bool Omega)
sigma F is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
a is Dynkin_System of Omega
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
a is non empty Element of bool I
(Omega,I,a,Sigma) is Element of bool I
F is set
T is Event of I
Sigma . T is ext-real V14() real Element of REAL
Ie is Element of a
T /\ Ie is Event of I
Sigma . (T /\ Ie) is ext-real V14() real Element of REAL
Sigma . Ie is ext-real V14() real Element of REAL
(Sigma . T) * (Sigma . Ie) is ext-real V14() real set
u is Event of I
F is Event of I
T is Event of I
u is Element of I
Ie is Element of a
u /\ Ie is Event of I
Sigma . (u /\ Ie) is ext-real V14() real Element of REAL
Sigma . u is ext-real V14() real Element of REAL
Sigma . Ie is ext-real V14() real Element of REAL
(Sigma . u) * (Sigma . Ie) is ext-real V14() real set
F is Event of I
T is Event of I
Ie is Event of I
u is Event of I
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is non empty Element of bool I
a is non empty Element of bool I
(Omega,I,a,Sigma) is Element of bool I
(Omega,I,P,Sigma) is Element of bool I
F is Event of I
T is Event of I
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is Element of bool (bool Omega)
sigma P is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
F is non empty Element of bool I
(Omega,I,F,Sigma) is Element of bool I
T is Element of bool (bool Omega)
sigma T is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
Ie is non empty Element of bool I
(Omega,I,Ie,Sigma) is Element of bool I
u is Element of bool (bool Omega)
a is non empty Element of bool I
(Omega,I,a,Sigma) is Element of bool I
sigma u is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty Relation-like I -defined REAL -valued Function-like V26(I) V30(I, REAL ) V33() V34() V35() V42() Probability of I
P is Element of bool (bool Omega)
sigma P is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
a is Element of bool (bool Omega)
sigma a is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
T is non empty Element of bool I
F is non empty Element of bool I
(Omega,I,F,Sigma) is Element of bool I
u is Element of bool (bool Omega)
sigma u is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
Ie is Element of bool (bool Omega)
sigma Ie is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
v is non empty Element of bool I
(Omega,I,v,Sigma) is Element of bool I
x is Event of I
E is Event of I
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
[:Omega,(bool Sigma):] is Relation-like set
bool [:Omega,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega --> Sigma is Relation-like Omega -defined bool (bool I) -valued Function-like V26(Omega) V30(Omega, bool (bool I)) Element of bool [:Omega,(bool (bool I)):]
[:Omega,(bool (bool I)):] is Relation-like set
bool [:Omega,(bool (bool I)):] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (Omega --> Sigma) is Element of bool (bool (bool I))
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
a is set
dom (Omega --> Sigma) is Element of bool Omega
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
F is set
(Omega --> Sigma) . F is set
a is set
(Omega --> Sigma) . a is set
dom (Omega --> Sigma) is Element of bool Omega
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
P is set
[:P,I:] is Relation-like set
bool [:P,I:] is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is set
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is Element of bool Sigma
[:P,I:] is Relation-like set
bool [:P,I:] is non empty cup-closed intersection_stable diff-closed preBoolean set
a is Relation-like Sigma -defined bool I -valued Function-like V26(Sigma) V30(Sigma, bool I) (Sigma,Omega,I)
P --> {} is Relation-like P -defined {{}} -valued Function-like V26(P) V30(P,{{}}) V33() V34() V35() V36() Element of bool [:P,{{}}:]
{{}} is non empty functional finite V52() V79() V80() V81() V82() V83() V84() set
[:P,{{}}:] is Relation-like RAT -valued INT -valued V33() V34() V35() V36() set
bool [:P,{{}}:] is non empty cup-closed intersection_stable diff-closed preBoolean set
T is set
(P --> {}) . T is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real Relation-like Function-like set
a . T is Element of bool (bool Omega)
dom (P --> {}) is Element of bool P
bool P is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (P --> {}) is V79() V80() V81() V82() V83() V84() Element of bool REAL
T is set
Ie is set
(P --> {}) . Ie is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real Relation-like Function-like set
a . Ie is Element of bool (bool Omega)
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
P is set
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
a is Element of bool Omega
P | a is Relation-like a -defined Omega -defined bool Sigma -valued Function-like set
[:a,(bool Sigma):] is Relation-like set
bool [:a,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty set
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is Element of bool Omega
P is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Sigma)
bool P is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool P)
bool P is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool P) is non empty cup-closed intersection_stable diff-closed preBoolean set
[:I,(bool P):] is Relation-like set
bool [:I,(bool P):] is non empty cup-closed intersection_stable diff-closed preBoolean set
a is Relation-like I -defined bool P -valued Function-like V26(I) V30(I, bool P) Element of bool [:I,(bool P):]
Union a is set
rng a is set
union (rng a) is set
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
F is set
dom a is Element of bool I
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
T is set
a . T is Element of bool (bool Sigma)
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
a is Element of bool Omega
P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(Omega,I,Sigma,P,a) is Relation-like a -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(a) V30(a, bool Sigma) Element of bool [:a,(bool Sigma):]
[:a,(bool Sigma):] is Relation-like set
bool [:a,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,a,I,Sigma,(Omega,I,Sigma,P,a)) is Element of bool (bool I)
rng (Omega,I,Sigma,P,a) is set
union (rng (Omega,I,Sigma,P,a)) is set
sigma (Omega,a,I,Sigma,(Omega,I,Sigma,P,a)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
bool (bool I) is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool (bool I))
a is set
{} Omega is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Omega
Omega \ ({} Omega) is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ ({} Omega))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ ({} Omega))) is Relation-like Omega \ ({} Omega) -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ ({} Omega)) V30(Omega \ ({} Omega), bool Sigma) Element of bool [:(Omega \ ({} Omega)),(bool Sigma):]
[:(Omega \ ({} Omega)),(bool Sigma):] is Relation-like set
bool [:(Omega \ ({} Omega)),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ ({} Omega)),I,Sigma,(Omega,I,Sigma,P,(Omega \ ({} Omega)))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ ({} Omega))) is set
union (rng (Omega,I,Sigma,P,(Omega \ ({} Omega)))) is set
sigma (Omega,(Omega \ ({} Omega)),I,Sigma,(Omega,I,Sigma,P,(Omega \ ({} Omega)))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
F is set
F is non empty Element of bool (bool (bool I))
T is Element of bool (bool I)
Ie is finite Element of bool Omega
Omega \ Ie is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ Ie)) is Relation-like Omega \ Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ Ie) V30(Omega \ Ie, bool Sigma) Element of bool [:(Omega \ Ie),(bool Sigma):]
[:(Omega \ Ie),(bool Sigma):] is Relation-like set
bool [:(Omega \ Ie),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ Ie)) is set
union (rng (Omega,I,Sigma,P,(Omega \ Ie))) is set
sigma (Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
a is Element of bool (bool (bool I))
F is Element of bool (bool (bool I))
T is Element of bool (bool I)
Ie is finite Element of bool Omega
Omega \ Ie is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ Ie)) is Relation-like Omega \ Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ Ie) V30(Omega \ Ie, bool Sigma) Element of bool [:(Omega \ Ie),(bool Sigma):]
[:(Omega \ Ie),(bool Sigma):] is Relation-like set
bool [:(Omega \ Ie),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ Ie)) is set
union (rng (Omega,I,Sigma,P,(Omega \ Ie))) is set
sigma (Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
Ie is finite Element of bool Omega
Omega \ Ie is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ Ie)) is Relation-like Omega \ Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ Ie) V30(Omega \ Ie, bool Sigma) Element of bool [:(Omega \ Ie),(bool Sigma):]
[:(Omega \ Ie),(bool Sigma):] is Relation-like set
bool [:(Omega \ Ie),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ Ie)) is set
union (rng (Omega,I,Sigma,P,(Omega \ Ie))) is set
sigma (Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(Omega,I,Sigma,P) is Element of bool (bool (bool I))
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
{} Omega is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Omega
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega \ ({} Omega) is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ ({} Omega))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ ({} Omega))) is Relation-like Omega \ ({} Omega) -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ ({} Omega)) V30(Omega \ ({} Omega), bool Sigma) Element of bool [:(Omega \ ({} Omega)),(bool Sigma):]
[:(Omega \ ({} Omega)),(bool Sigma):] is Relation-like set
bool [:(Omega \ ({} Omega)),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ ({} Omega)),I,Sigma,(Omega,I,Sigma,P,(Omega \ ({} Omega)))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ ({} Omega))) is set
union (rng (Omega,I,Sigma,P,(Omega \ ({} Omega)))) is set
sigma (Omega,(Omega \ ({} Omega)),I,Sigma,(Omega,I,Sigma,P,(Omega \ ({} Omega)))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(Omega,I,Sigma,P) is non empty Element of bool (bool (bool I))
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
meet (Omega,I,Sigma,P) is Element of bool (bool I)
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(Omega,I,Sigma,P) is Element of bool (bool I)
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
(Omega,I,Sigma,P) is non empty Element of bool (bool (bool I))
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
meet (Omega,I,Sigma,P) is Element of bool (bool I)
a is set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
F is finite Element of bool Omega
Omega \ F is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ F)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ F)) is Relation-like Omega \ F -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ F) V30(Omega \ F, bool Sigma) Element of bool [:(Omega \ F),(bool Sigma):]
[:(Omega \ F),(bool Sigma):] is Relation-like set
bool [:(Omega \ F),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ F),I,Sigma,(Omega,I,Sigma,P,(Omega \ F))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ F)) is set
union (rng (Omega,I,Sigma,P,(Omega \ F))) is set
sigma (Omega,(Omega \ F),I,Sigma,(Omega,I,Sigma,P,(Omega \ F))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty set
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
a is non empty Relation-like Sigma -defined bool I -valued Function-like V26(Sigma) V30(Sigma, bool I) (Sigma,Omega,I)
P is non empty Element of bool Sigma
bool Omega is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Omega)
F is set
T is set
T is Element of bool (bool Omega)
Ie is Element of bool Omega
u is non empty finite Element of bool Sigma
v is non empty Relation-like u -defined I -valued Function-like V26(u) V30(u,I) finite (Omega,I,Sigma,u,a)
rng v is non empty finite Element of bool I
meet (rng v) is set
F is Element of bool (bool Omega)
T is Element of bool (bool Omega)
Ie is Element of bool Omega
u is non empty finite Element of bool Sigma
v is non empty Relation-like u -defined I -valued Function-like V26(u) V30(u,I) finite (Omega,I,Sigma,u,a)
rng v is non empty finite Element of bool I
meet (rng v) is set
u is non empty finite Element of bool Sigma
v is non empty Relation-like u -defined I -valued Function-like V26(u) V30(u,I) finite (Omega,I,Sigma,u,a)
rng v is non empty finite Element of bool I
meet (rng v) is set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is non empty Relation-like I -defined bool Sigma -valued Function-like V26(I) V30(I, bool Sigma) (I,Omega,Sigma)
a is non empty Element of bool I
(Omega,Sigma,I,a,P) is Element of bool (bool Omega)
sigma (Omega,Sigma,I,a,P) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,P,a) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,P,a) is non empty Relation-like a -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(a) V30(a, bool Sigma) Element of bool [:a,(bool Sigma):]
[:a,(bool Sigma):] is non empty Relation-like set
bool [:a,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,a,Omega,Sigma,(I,Omega,Sigma,P,a)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,P,a) is non empty set
union (rng (I,Omega,Sigma,P,a)) is set
sigma (I,a,Omega,Sigma,(I,Omega,Sigma,P,a)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
F is set
rng (I,Omega,Sigma,P,a) is non empty Element of bool (bool Sigma)
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
T is set
dom (I,Omega,Sigma,P,a) is non empty Element of bool a
bool a is non empty cup-closed intersection_stable diff-closed preBoolean set
Ie is set
(I,Omega,Sigma,P,a) . Ie is Element of bool (bool Omega)
u is Element of bool Omega
{Ie} is non empty finite set
v is finite Element of bool I
x is set
P . x is Element of bool (bool Omega)
P . Ie is Element of bool (bool Omega)
E is Element of bool Omega
[:v,Sigma:] is Relation-like set
bool [:v,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
x is Relation-like v -defined Sigma -valued Function-like V26(v) V30(v,Sigma) finite Element of bool [:v,Sigma:]
E is set
x . E is set
P . E is Element of bool (bool Omega)
E is Relation-like v -defined Sigma -valued Function-like V26(v) V30(v,Sigma) finite (Omega,Sigma,I,v,P)
dom E is finite Element of bool v
bool v is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
rng E is finite Element of bool Sigma
E . Ie is set
{(E . Ie)} is non empty finite set
meet (rng E) is set
F is set
T is non empty finite Element of bool I
Ie is non empty Relation-like T -defined Sigma -valued Function-like V26(T) V30(T,Sigma) finite (Omega,Sigma,I,T,P)
rng Ie is non empty finite Element of bool Sigma
meet (rng Ie) is set
Fin T is non empty cup-closed diff-closed preBoolean set
v is finite Element of Fin T
Ie | v is Relation-like T -defined v -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
[:T,Sigma:] is non empty Relation-like set
bool [:T,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (Ie | v) is finite Element of bool Sigma
meet (rng (Ie | v)) is set
x is finite Element of Fin T
Ie | x is Relation-like T -defined x -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
rng (Ie | x) is finite Element of bool Sigma
meet (rng (Ie | x)) is set
E is Element of T
{E} is non empty finite set
x \/ {E} is non empty finite set
Ie | (x \/ {E}) is Relation-like T -defined x \/ {E} -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
rng (Ie | (x \/ {E})) is finite Element of bool Sigma
meet (rng (Ie | (x \/ {E}))) is set
Ie | {E} is Relation-like T -defined {E} -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
rng (Ie | {E}) is finite Element of bool Sigma
(Ie | x) \/ (Ie | {E}) is Relation-like T -defined Sigma -valued finite Element of bool [:T,Sigma:]
rng ((Ie | x) \/ (Ie | {E})) is finite Element of bool Sigma
(rng (Ie | x)) \/ (rng (Ie | {E})) is finite Element of bool Sigma
dom (I,Omega,Sigma,P,a) is non empty Element of bool a
bool a is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,Omega,Sigma,P,a) . E is Element of bool (bool Omega)
rng (I,Omega,Sigma,P,a) is non empty Element of bool (bool Sigma)
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P . E is Element of bool (bool Omega)
dom Ie is non empty finite Element of bool T
bool T is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
(dom Ie) /\ {E} is finite Element of bool T
dom (Ie | {E}) is finite Element of bool T
(Ie | {E}) . E is set
{((Ie | {E}) . E)} is non empty finite set
Ie . E is Element of Sigma
{(Ie . E)} is non empty finite set
meet (rng (Ie | {E})) is set
y is set
E2 is set
meet E2 is set
E1 is set
meet E1 is set
meet y is set
(meet E1) /\ (meet y) is set
Ie | {} is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined {} -defined T -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:T,Sigma:]
rng (Ie | {}) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool REAL
meet (rng (Ie | {})) is set
{}. T is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of Fin T
Ie | ({}. T) is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined T -defined {}. T -defined T -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:T,Sigma:]
rng (Ie | ({}. T)) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Sigma
meet (rng (Ie | ({}. T))) is set
u is finite Element of Fin T
Ie | u is Relation-like T -defined u -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
[:T,Sigma:] is non empty Relation-like set
bool [:T,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (Ie | u) is finite Element of bool Sigma
meet (rng (Ie | u)) is set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is non empty Relation-like Sigma -defined REAL -valued Function-like V26(Sigma) V30(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
a is non empty Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
F is non empty Element of bool Omega
T is non empty Element of bool Omega
(I,Sigma,Omega,F,a) is Element of bool (bool I)
(I,Sigma,Omega,T,a) is Element of bool (bool I)
u is Element of bool I
v is Element of bool I
u /\ v is Element of bool I
P . (u /\ v) is ext-real V14() real set
P . u is ext-real V14() real set
P . v is ext-real V14() real set
(P . u) * (P . v) is ext-real V14() real set
x is non empty finite Element of bool Omega
E is non empty Relation-like x -defined Sigma -valued Function-like V26(x) V30(x,Sigma) finite (I,Sigma,Omega,x,a)
rng E is non empty finite Element of bool Sigma
meet (rng E) is set
y is non empty finite Element of bool Omega
E1 is non empty Relation-like y -defined Sigma -valued Function-like V26(y) V30(y,Sigma) finite (I,Sigma,Omega,y,a)
rng E1 is non empty finite Element of bool Sigma
meet (rng E1) is set
E2 is set
[:x,E2:] is Relation-like set
bool [:x,E2:] is non empty cup-closed intersection_stable diff-closed preBoolean set
E3 is set
[:y,E3:] is Relation-like set
bool [:y,E3:] is non empty cup-closed intersection_stable diff-closed preBoolean set
i is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
Seg i is finite V55(i) V79() V80() V81() V82() V83() V84() Element of bool NAT
z is Relation-like Function-like set
dom z is set
rng z is set
[:(Seg i),y:] is Relation-like finite set
bool [:(Seg i),y:] is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
B9 is Relation-like Seg i -defined y -valued Function-like V26( Seg i) V30( Seg i,y) finite Element of bool [:(Seg i),y:]
S is Relation-like y -defined E3 -valued Function-like V30(y,E3) finite Element of bool [:y,E3:]
S * B9 is Relation-like Seg i -defined E3 -valued Function-like V30( Seg i,E3) finite Element of bool [:(Seg i),E3:]
[:(Seg i),E3:] is Relation-like set
bool [:(Seg i),E3:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (S * B9) is finite Element of bool E3
bool E3 is non empty cup-closed intersection_stable diff-closed preBoolean set
rng S is finite Element of bool E3
Ie is set
[:y,Ie:] is Relation-like set
bool [:y,Ie:] is non empty cup-closed intersection_stable diff-closed preBoolean set
f2 is Relation-like y -defined Ie -valued Function-like V30(y,Ie) finite Element of bool [:y,Ie:]
b is Relation-like NAT -defined y -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of y
f2 * b is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
rng b is finite Element of bool y
bool y is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
dom f2 is finite Element of bool y
fe2 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
len fe2 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
len b is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
x \/ y is non empty finite Element of bool Omega
n is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
Seg n is finite V55(n) V79() V80() V81() V82() V83() V84() Element of bool NAT
e1 is Relation-like Function-like set
dom e1 is set
rng e1 is set
[:(Seg n),x:] is Relation-like finite set
bool [:(Seg n),x:] is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
e1 is Relation-like Seg n -defined x -valued Function-like V26( Seg n) V30( Seg n,x) finite Element of bool [:(Seg n),x:]
X is Relation-like x -defined E2 -valued Function-like V30(x,E2) finite Element of bool [:x,E2:]
X * e1 is Relation-like Seg n -defined E2 -valued Function-like V30( Seg n,E2) finite Element of bool [:(Seg n),E2:]
[:(Seg n),E2:] is Relation-like set
bool [:(Seg n),E2:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (X * e1) is finite Element of bool E2
bool E2 is non empty cup-closed intersection_stable diff-closed preBoolean set
rng X is finite Element of bool E2
[:x,Ie:] is Relation-like set
bool [:x,Ie:] is non empty cup-closed intersection_stable diff-closed preBoolean set
f1 is Relation-like x -defined Ie -valued Function-like V30(x,Ie) finite Element of bool [:x,Ie:]
e1 is Relation-like NAT -defined x -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of x
f1 * e1 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
rng e1 is finite Element of bool x
bool x is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
dom f1 is finite Element of bool x
fe1 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
len fe1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
len e1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
h is Relation-like Function-like set
dom h is set
e1 ^ b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (e1 ^ b) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
(e1 ^ b) (#) h is Relation-like NAT -defined Function-like finite set
dom ((e1 ^ b) (#) h) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
h is set
rng (e1 ^ b) is finite set
(e1 ^ b) . h is set
h is set
fe1 ^ fe2 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
dom (fe1 ^ fe2) is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
(len fe1) + (len fe2) is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
Seg ((len fe1) + (len fe2)) is finite V55((len fe1) + (len fe2)) V79() V80() V81() V82() V83() V84() Element of bool NAT
h is set
(fe1 ^ fe2) . h is set
((e1 ^ b) (#) h) . h is set
h is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
dom fe1 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
(fe1 ^ fe2) . h is set
fe1 . h is set
dom e1 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
e1 . h is set
h . (e1 . h) is set
f1 . (e1 . h) is set
(e1 ^ b) . h is set
h is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
dom fe1 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
dom fe2 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
Pfe1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
(len fe1) + Pfe1 is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
dom b is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
b . Pfe1 is set
x /\ y is finite Element of bool Omega
F /\ T is Element of bool Omega
y \ x is finite Element of bool Omega
(y \ x) \/ {} is finite set
(fe1 ^ fe2) . h is set
fe2 . Pfe1 is set
f2 . (b . Pfe1) is set
h . (b . Pfe1) is set
(e1 ^ b) . h is set
h . ((e1 ^ b) . h) is set
h is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
dom fe1 is finite V79() V80() V81() V82() V83() V84() Element of bool NAT
h is set
h . h is set
f1 . h is set
f2 . h is set
[:(x \/ y),Sigma:] is non empty Relation-like set
bool [:(x \/ y),Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
h is non empty Relation-like x \/ y -defined Sigma -valued Function-like V26(x \/ y) V30(x \/ y,Sigma) finite Element of bool [:(x \/ y),Sigma:]
h is set
h . h is set
a . h is Element of bool (bool I)
f1 . h is set
f2 . h is set
h is non empty Relation-like x \/ y -defined Sigma -valued Function-like V26(x \/ y) V30(x \/ y,Sigma) finite (I,Sigma,Omega,x \/ y,a)
P * f1 is Relation-like x -defined REAL -valued Function-like V33() V34() V35() finite Element of bool [:x,REAL:]
[:x,REAL:] is non empty Relation-like V33() V34() V35() set
bool [:x,REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
(P * f1) * e1 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite Element of bool [:NAT,REAL:]
P * f2 is Relation-like y -defined REAL -valued Function-like V33() V34() V35() finite Element of bool [:y,REAL:]
[:y,REAL:] is non empty Relation-like V33() V34() V35() set
bool [:y,REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
(P * f2) * b is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite Element of bool [:NAT,REAL:]
x /\ y is finite Element of bool Omega
F /\ T is Element of bool Omega
e1 is Relation-like NAT -defined x \/ y -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x \/ y
rng e1 is finite Element of bool (x \/ y)
bool (x \/ y) is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
e2 is Relation-like NAT -defined x \/ y -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x \/ y
rng e2 is finite Element of bool (x \/ y)
e1 ^ e2 is Relation-like NAT -defined x \/ y -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x \/ y
[:x,Sigma:] is non empty Relation-like set
bool [:x,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:y,Sigma:] is non empty Relation-like set
bool [:y,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
[:Ie,REAL:] is Relation-like V33() V34() V35() set
bool [:Ie,REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
e12 is Relation-like NAT -defined x \/ y -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of x \/ y
P is Relation-like Ie -defined REAL -valued Function-like V26(Ie) V30(Ie, REAL ) V33() V34() V35() Element of bool [:Ie,REAL:]
P * h is Relation-like x \/ y -defined REAL -valued Function-like V33() V34() V35() finite Element of bool [:(x \/ y),REAL:]
[:(x \/ y),REAL:] is non empty Relation-like V33() V34() V35() set
bool [:(x \/ y),REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
(P * h) * e12 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite Element of bool [:NAT,REAL:]
e1 is Relation-like NAT -defined x -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of x
e2 is Relation-like NAT -defined y -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of y
e1 ^ e2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(e1 ^ e2) (#) h is Relation-like NAT -defined Sigma -valued Function-like finite set
((e1 ^ e2) (#) h) (#) P is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite set
fe1 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
P * fe1 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of REAL
fe2 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
P * fe2 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of REAL
(P * fe1) ^ (P * fe2) is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Pfe1 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Pfe2 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of REAL
[:Sigma,REAL:] is non empty Relation-like V33() V34() V35() set
bool [:Sigma,REAL:] is non empty cup-closed intersection_stable diff-closed preBoolean set
f1 is non empty Relation-like x -defined Sigma -valued Function-like V26(x) V30(x,Sigma) finite Element of bool [:x,Sigma:]
P is non empty Relation-like Sigma -defined REAL -valued Function-like V26(Sigma) V30(Sigma, REAL ) V33() V34() V35() Element of bool [:Sigma,REAL:]
P * f1 is non empty Relation-like x -defined REAL -valued Function-like V26(x) V30(x, REAL ) V33() V34() V35() finite Element of bool [:x,REAL:]
(P * f1) * e1 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Product ((P * f1) * e1) is ext-real V14() real Element of REAL
f1 * e1 is Relation-like NAT -defined Sigma -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Sigma
rng (f1 * e1) is finite Element of bool Sigma
meet (rng (f1 * e1)) is set
P . (meet (rng (f1 * e1))) is ext-real V14() real set
P . (u /\ v) is ext-real V14() real set
rng f1 is non empty finite Element of bool Sigma
f2 is non empty Relation-like y -defined Sigma -valued Function-like V26(y) V30(y,Sigma) finite Element of bool [:y,Sigma:]
rng f2 is non empty finite Element of bool Sigma
(rng f1) \/ (rng f2) is non empty finite Element of bool Sigma
meet ((rng f1) \/ (rng f2)) is set
P . (meet ((rng f1) \/ (rng f2))) is ext-real V14() real set
fe1 ^ fe2 is Relation-like NAT -defined Ie -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Ie
rng (fe1 ^ fe2) is finite Element of bool Ie
bool Ie is non empty cup-closed intersection_stable diff-closed preBoolean set
meet (rng (fe1 ^ fe2)) is set
P . (meet (rng (fe1 ^ fe2))) is ext-real V14() real set
Pfe1 ^ Pfe2 is Relation-like NAT -defined REAL -valued Function-like V33() V34() V35() finite FinSequence-like FinSubsequence-like FinSequence of REAL
Product (Pfe1 ^ Pfe2) is ext-real V14() real Element of REAL
Product Pfe1 is ext-real V14() real Element of REAL
Product Pfe2 is ext-real V14() real Element of REAL
(Product Pfe1) * (Product Pfe2) is ext-real V14() real set
P . u is ext-real V14() real set
P . v is ext-real V14() real set
(P . u) * (P . v) is ext-real V14() real set
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is non empty Relation-like I -defined bool Sigma -valued Function-like V26(I) V30(I, bool Sigma) (I,Omega,Sigma)
a is non empty Element of bool I
(Omega,Sigma,I,a,P) is Element of bool (bool Omega)
F is set
T is non empty finite Element of bool I
Ie is non empty Relation-like T -defined Sigma -valued Function-like V26(T) V30(T,Sigma) finite (Omega,Sigma,I,T,P)
rng Ie is non empty finite Element of bool Sigma
meet (rng Ie) is set
Fin T is non empty cup-closed diff-closed preBoolean set
v is finite Element of Fin T
Ie | v is Relation-like T -defined v -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
[:T,Sigma:] is non empty Relation-like set
bool [:T,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (Ie | v) is finite Element of bool Sigma
meet (rng (Ie | v)) is set
x is finite Element of Fin T
Ie | x is Relation-like T -defined x -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
rng (Ie | x) is finite Element of bool Sigma
meet (rng (Ie | x)) is set
E is Element of T
{E} is non empty finite set
x \/ {E} is non empty finite set
Ie | (x \/ {E}) is Relation-like T -defined x \/ {E} -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
rng (Ie | (x \/ {E})) is finite Element of bool Sigma
meet (rng (Ie | (x \/ {E}))) is set
Ie | {E} is Relation-like T -defined {E} -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
(Ie | x) \/ (Ie | {E}) is Relation-like T -defined Sigma -valued finite Element of bool [:T,Sigma:]
rng ((Ie | x) \/ (Ie | {E})) is finite Element of bool Sigma
rng (Ie | {E}) is finite Element of bool Sigma
(rng (Ie | x)) \/ (rng (Ie | {E})) is finite Element of bool Sigma
dom Ie is non empty finite Element of bool T
bool T is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
Ie . E is Element of Sigma
(dom Ie) /\ {E} is finite Element of bool T
dom (Ie | {E}) is finite Element of bool T
(Ie | {E}) . E is set
{((Ie | {E}) . E)} is non empty finite set
{(Ie . E)} is non empty finite set
meet (rng (Ie | {E})) is set
(meet (rng (Ie | x))) /\ (meet (rng (Ie | {E}))) is set
Ie | {} is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined {} -defined T -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:T,Sigma:]
rng (Ie | {}) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool REAL
meet (rng (Ie | {})) is set
{}. T is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of Fin T
Ie | ({}. T) is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined T -defined {}. T -defined T -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:T,Sigma:]
rng (Ie | ({}. T)) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Sigma
meet (rng (Ie | ({}. T))) is set
u is finite Element of Fin T
Ie | u is Relation-like T -defined u -defined T -defined Sigma -valued Function-like finite Element of bool [:T,Sigma:]
[:T,Sigma:] is non empty Relation-like set
bool [:T,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (Ie | u) is finite Element of bool Sigma
meet (rng (Ie | u)) is set
bool a is non empty cup-closed intersection_stable diff-closed preBoolean set
the non empty finite Element of bool a is non empty finite Element of bool a
{{}} is non empty functional finite V52() V79() V80() V81() V82() V83() V84() set
T is Relation-like Function-like set
dom T is set
rng T is set
meet (rng T) is set
u is set
Ie is non empty finite Element of bool I
[:Ie,Sigma:] is non empty Relation-like set
bool [:Ie,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
u is non empty Relation-like Ie -defined Sigma -valued Function-like V26(Ie) V30(Ie,Sigma) finite Element of bool [:Ie,Sigma:]
v is set
u . v is set
P . v is Element of bool (bool Omega)
rng u is non empty finite Element of bool Sigma
x is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
v is non empty Relation-like Ie -defined Sigma -valued Function-like V26(Ie) V30(Ie,Sigma) finite (Omega,Sigma,I,Ie,P)
rng v is non empty finite Element of bool Sigma
meet (rng v) is set
x is Element of bool Omega
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is non empty set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
a is non empty Element of bool Omega
P is non empty Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(I,Sigma,Omega,a,P) is Element of bool (bool I)
F is set
T is set
F /\ T is set
Ie is non empty finite Element of bool Omega
u is non empty Relation-like Ie -defined Sigma -valued Function-like V26(Ie) V30(Ie,Sigma) finite (I,Sigma,Omega,Ie,P)
rng u is non empty finite Element of bool Sigma
meet (rng u) is set
v is non empty finite Element of bool Omega
x is non empty Relation-like v -defined Sigma -valued Function-like V26(v) V30(v,Sigma) finite (I,Sigma,Omega,v,P)
rng x is non empty finite Element of bool Sigma
meet (rng x) is set
Ie \ v is finite Element of bool Omega
v \ Ie is finite Element of bool Omega
(Ie \ v) \/ (v \ Ie) is finite Element of bool Omega
Ie \/ v is non empty finite Element of bool Omega
E is Relation-like Function-like set
dom E is set
y is Relation-like Function-like set
dom y is set
E1 is set
y . E1 is set
P . E1 is Element of bool (bool I)
E . E1 is set
u . E1 is set
x . E1 is set
Ie \+\ v is finite Element of bool Omega
Ie \ v is finite set
v \ Ie is finite set
(Ie \ v) \/ (v \ Ie) is finite set
u . E1 is set
x . E1 is set
(u . E1) /\ (x . E1) is set
E2 is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
rng y is set
E1 is set
E2 is set
y . E2 is set
P . E2 is Element of bool (bool I)
[:(Ie \/ v),Sigma:] is non empty Relation-like set
bool [:(Ie \/ v),Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
E1 is non empty Relation-like Ie \/ v -defined Sigma -valued Function-like V26(Ie \/ v) V30(Ie \/ v,Sigma) finite (I,Sigma,Omega,Ie \/ v,P)
rng E1 is non empty finite Element of bool Sigma
meet (rng E1) is set
Ie /\ v is finite Element of bool Omega
E1 | (Ie /\ v) is Relation-like Ie \/ v -defined Ie /\ v -defined Ie \/ v -defined Sigma -valued Function-like finite Element of bool [:(Ie \/ v),Sigma:]
rng (E1 | (Ie /\ v)) is finite Element of bool Sigma
meet (rng (E1 | (Ie /\ v))) is set
u | (Ie /\ v) is Relation-like Ie -defined Ie /\ v -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
[:Ie,Sigma:] is non empty Relation-like set
bool [:Ie,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (u | (Ie /\ v)) is finite Element of bool Sigma
meet (rng (u | (Ie /\ v))) is set
x | (Ie /\ v) is Relation-like v -defined Ie /\ v -defined v -defined Sigma -valued Function-like finite Element of bool [:v,Sigma:]
[:v,Sigma:] is non empty Relation-like set
bool [:v,Sigma:] is non empty cup-closed intersection_stable diff-closed preBoolean set
rng (x | (Ie /\ v)) is finite Element of bool Sigma
meet (rng (x | (Ie /\ v))) is set
(meet (rng (u | (Ie /\ v)))) /\ (meet (rng (x | (Ie /\ v)))) is set
rng {} is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool REAL
meet (rng {}) is set
E2 is non empty set
Fin E2 is non empty cup-closed diff-closed preBoolean set
X is finite Element of Fin E2
E1 | X is Relation-like Ie \/ v -defined X -defined Ie \/ v -defined Sigma -valued Function-like finite Element of bool [:(Ie \/ v),Sigma:]
rng (E1 | X) is finite Element of bool Sigma
meet (rng (E1 | X)) is set
u | X is Relation-like Ie -defined X -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
rng (u | X) is finite Element of bool Sigma
meet (rng (u | X)) is set
x | X is Relation-like v -defined X -defined v -defined Sigma -valued Function-like finite Element of bool [:v,Sigma:]
rng (x | X) is finite Element of bool Sigma
meet (rng (x | X)) is set
(meet (rng (u | X))) /\ (meet (rng (x | X))) is set
S is finite Element of Fin E2
E1 | S is Relation-like Ie \/ v -defined S -defined Ie \/ v -defined Sigma -valued Function-like finite Element of bool [:(Ie \/ v),Sigma:]
rng (E1 | S) is finite Element of bool Sigma
meet (rng (E1 | S)) is set
u | S is Relation-like Ie -defined S -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
rng (u | S) is finite Element of bool Sigma
meet (rng (u | S)) is set
x | S is Relation-like v -defined S -defined v -defined Sigma -valued Function-like finite Element of bool [:v,Sigma:]
rng (x | S) is finite Element of bool Sigma
meet (rng (x | S)) is set
(meet (rng (u | S))) /\ (meet (rng (x | S))) is set
i is Element of E2
{i} is non empty finite set
S \/ {i} is non empty finite set
E1 | (S \/ {i}) is Relation-like Ie \/ v -defined S \/ {i} -defined Ie \/ v -defined Sigma -valued Function-like finite Element of bool [:(Ie \/ v),Sigma:]
rng (E1 | (S \/ {i})) is finite Element of bool Sigma
meet (rng (E1 | (S \/ {i}))) is set
u | (S \/ {i}) is Relation-like Ie -defined S \/ {i} -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
rng (u | (S \/ {i})) is finite Element of bool Sigma
meet (rng (u | (S \/ {i}))) is set
x | (S \/ {i}) is Relation-like v -defined S \/ {i} -defined v -defined Sigma -valued Function-like finite Element of bool [:v,Sigma:]
rng (x | (S \/ {i})) is finite Element of bool Sigma
meet (rng (x | (S \/ {i}))) is set
(meet (rng (u | (S \/ {i})))) /\ (meet (rng (x | (S \/ {i})))) is set
u | {i} is Relation-like Ie -defined {i} -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
dom (u | {i}) is finite Element of bool Ie
bool Ie is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
dom u is non empty finite Element of bool Ie
(dom u) /\ {i} is finite Element of bool Ie
rng (u | {i}) is finite Element of bool Sigma
(u | {i}) . i is set
{((u | {i}) . i)} is non empty finite set
Ie \ (Ie \/ v) is finite Element of bool Omega
Ie /\ Ie is finite Element of bool Omega
(Ie /\ Ie) /\ v is finite Element of bool Omega
(Ie \ (Ie \/ v)) \/ ((Ie /\ Ie) /\ v) is finite Element of bool Omega
Ie \+\ v is finite Element of bool Omega
Ie \ v is finite set
v \ Ie is finite set
(Ie \ v) \/ (v \ Ie) is finite set
Ie \ (Ie \+\ v) is finite Element of bool Omega
u . i is set
{(u . i)} is non empty finite set
meet (rng (u | {i})) is set
x | {i} is Relation-like v -defined {i} -defined v -defined Sigma -valued Function-like finite Element of bool [:v,Sigma:]
dom (x | {i}) is finite Element of bool v
bool v is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
dom x is non empty finite Element of bool v
(dom x) /\ {i} is finite Element of bool v
rng (x | {i}) is finite Element of bool Sigma
(x | {i}) . i is set
{((x | {i}) . i)} is non empty finite set
x . i is set
{(x . i)} is non empty finite set
meet (rng (x | {i})) is set
z is Relation-like Function-like set
B9 is set
b is set
{b} is non empty finite set
B9 \/ {b} is non empty set
z | (B9 \/ {b}) is Relation-like Function-like set
rng (z | (B9 \/ {b})) is set
meet (rng (z | (B9 \/ {b}))) is set
z | B9 is Relation-like Function-like set
rng (z | B9) is set
z | {b} is Relation-like Function-like finite set
rng (z | {b}) is finite set
(rng (z | B9)) \/ (rng (z | {b})) is set
meet ((rng (z | B9)) \/ (rng (z | {b}))) is set
(z | B9) \/ (z | {b}) is Relation-like set
rng ((z | B9) \/ (z | {b})) is set
dom E1 is non empty finite Element of bool (Ie \/ v)
bool (Ie \/ v) is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
(dom E1) /\ {i} is finite Element of bool (Ie \/ v)
E1 | {i} is Relation-like Ie \/ v -defined {i} -defined Ie \/ v -defined Sigma -valued Function-like finite Element of bool [:(Ie \/ v),Sigma:]
dom (E1 | {i}) is finite Element of bool {i}
bool {i} is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
rng (E1 | {i}) is finite Element of bool Sigma
(E1 | {i}) . i is set
{((E1 | {i}) . i)} is non empty finite set
E1 . i is set
{(E1 . i)} is non empty finite set
meet (rng (E1 | {i})) is set
(u . i) /\ (x . i) is set
the Element of S is Element of S
dom (E1 | S) is finite Element of bool S
bool S is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
(rng (E1 | S)) \/ (rng (E1 | {i})) is finite Element of bool Sigma
meet ((rng (E1 | S)) \/ (rng (E1 | {i}))) is set
(meet (rng (E1 | S))) /\ (meet (rng (E1 | {i}))) is set
((meet (rng (u | S))) /\ (meet (rng (x | S)))) /\ (E1 . i) is set
(meet (rng (x | S))) /\ ((u . i) /\ (x . i)) is set
(meet (rng (u | S))) /\ ((meet (rng (x | S))) /\ ((u . i) /\ (x . i))) is set
(meet (rng (x | S))) /\ (x . i) is set
(u . i) /\ ((meet (rng (x | S))) /\ (x . i)) is set
(meet (rng (u | S))) /\ ((u . i) /\ ((meet (rng (x | S))) /\ (x . i))) is set
(meet (rng (u | S))) /\ (u . i) is set
((meet (rng (u | S))) /\ (u . i)) /\ ((meet (rng (x | S))) /\ (x . i)) is set
(rng (u | S)) \/ (rng (u | {i})) is finite Element of bool Sigma
meet ((rng (u | S)) \/ (rng (u | {i}))) is set
(meet (rng (u | S))) /\ (meet (rng (u | {i}))) is set
(rng (x | S)) \/ (rng (x | {i})) is finite Element of bool Sigma
meet ((rng (x | S)) \/ (rng (x | {i}))) is set
(meet (rng (x | S))) /\ (meet (rng (x | {i}))) is set
{}. E2 is ext-real empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of Fin E2
E1 | ({}. E2) is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined Ie \/ v -defined {}. E2 -defined Ie \/ v -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:(Ie \/ v),Sigma:]
rng (E1 | ({}. E2)) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Sigma
meet (rng (E1 | ({}. E2))) is set
u | ({}. E2) is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined Ie -defined {}. E2 -defined Ie -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:Ie,Sigma:]
rng (u | ({}. E2)) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Sigma
meet (rng (u | ({}. E2))) is set
x | ({}. E2) is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined v -defined {}. E2 -defined v -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:v,Sigma:]
rng (x | ({}. E2)) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool Sigma
meet (rng (x | ({}. E2))) is set
(meet (rng (u | ({}. E2)))) /\ (meet (rng (x | ({}. E2)))) is set
E3 is finite Element of Fin E2
E1 | E3 is Relation-like Ie \/ v -defined E3 -defined Ie \/ v -defined Sigma -valued Function-like finite Element of bool [:(Ie \/ v),Sigma:]
rng (E1 | E3) is finite Element of bool Sigma
meet (rng (E1 | E3)) is set
u | E3 is Relation-like Ie -defined E3 -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
rng (u | E3) is finite Element of bool Sigma
meet (rng (u | E3)) is set
x | E3 is Relation-like v -defined E3 -defined v -defined Sigma -valued Function-like finite Element of bool [:v,Sigma:]
rng (x | E3) is finite Element of bool Sigma
meet (rng (x | E3)) is set
(meet (rng (u | E3))) /\ (meet (rng (x | E3))) is set
E2 is set
E3 is set
E2 \/ E3 is set
E2 /\ E3 is set
E2 \ E3 is Element of bool E2
bool E2 is non empty cup-closed intersection_stable diff-closed preBoolean set
E3 \ E2 is Element of bool E3
bool E3 is non empty cup-closed intersection_stable diff-closed preBoolean set
X is Relation-like Function-like set
dom X is set
rng X is set
X | (E2 /\ E3) is Relation-like Function-like set
rng (X | (E2 /\ E3)) is set
X | (E2 \ E3) is Relation-like Function-like set
rng (X | (E2 \ E3)) is set
(rng (X | (E2 /\ E3))) \/ (rng (X | (E2 \ E3))) is set
X | (E3 \ E2) is Relation-like Function-like set
rng (X | (E3 \ E2)) is set
((rng (X | (E2 /\ E3))) \/ (rng (X | (E2 \ E3)))) \/ (rng (X | (E3 \ E2))) is set
S is set
i is set
X . i is set
(E2 \ E3) \/ (E3 \ E2) is set
E2 /\ ((E2 \ E3) \/ (E3 \ E2)) is set
E2 /\ (E2 \ E3) is Element of bool E2
E2 /\ (E3 \ E2) is Element of bool E3
(E2 /\ (E2 \ E3)) \/ (E2 /\ (E3 \ E2)) is set
(E2 \ E3) \/ (E2 /\ (E3 \ E2)) is set
(E2 /\ E3) \ E2 is Element of bool (E2 /\ E3)
bool (E2 /\ E3) is non empty cup-closed intersection_stable diff-closed preBoolean set
(E2 \ E3) \/ ((E2 /\ E3) \ E2) is set
(E2 \ E3) \/ {} is set
(dom X) /\ (E2 \ E3) is Element of bool E2
dom (X | (E2 \ E3)) is set
(X | (E2 \ E3)) . i is set
((E2 \ E3) \/ (E3 \ E2)) \ E2 is Element of bool ((E2 \ E3) \/ (E3 \ E2))
bool ((E2 \ E3) \/ (E3 \ E2)) is non empty cup-closed intersection_stable diff-closed preBoolean set
(E2 \ E3) \ E2 is Element of bool E2
(E3 \ E2) \ E2 is Element of bool E3
((E2 \ E3) \ E2) \/ ((E3 \ E2) \ E2) is set
{} \/ ((E3 \ E2) \ E2) is set
E2 \/ E2 is set
E3 \ (E2 \/ E2) is Element of bool E3
(dom X) /\ (E3 \ E2) is Element of bool E3
dom (X | (E3 \ E2)) is set
(X | (E3 \ E2)) . i is set
(rng (X | (E2 \ E3))) \/ (rng (X | (E3 \ E2))) is set
(rng (X | (E2 /\ E3))) \/ ((rng (X | (E2 \ E3))) \/ (rng (X | (E3 \ E2)))) is set
(E2 \ E3) \/ (E3 \ E2) is set
E2 \+\ E3 is set
E2 \ E3 is set
E3 \ E2 is set
(E2 \ E3) \/ (E3 \ E2) is set
(E2 \/ E3) \ (E2 \+\ E3) is Element of bool (E2 \/ E3)
bool (E2 \/ E3) is non empty cup-closed intersection_stable diff-closed preBoolean set
(E2 \/ E3) \ (E2 \/ E3) is Element of bool (E2 \/ E3)
(E2 \/ E3) /\ E2 is set
((E2 \/ E3) /\ E2) /\ E3 is set
((E2 \/ E3) \ (E2 \/ E3)) \/ (((E2 \/ E3) /\ E2) /\ E3) is set
{} \/ (((E2 \/ E3) /\ E2) /\ E3) is set
(E2 \/ E3) /\ (E2 /\ E3) is set
dom (X | (E2 /\ E3)) is set
(X | (E2 /\ E3)) . i is set
(E2 \ E3) \/ (E3 \ E2) is set
E1 | (Ie \ v) is Relation-like Ie \ v -defined Ie \/ v -defined Sigma -valued Function-like finite Element of bool [:(Ie \/ v),Sigma:]
rng (E1 | (Ie \ v)) is finite Element of bool Sigma
(rng (E1 | (Ie /\ v))) \/ (rng (E1 | (Ie \ v))) is finite Element of bool Sigma
E1 | (v \ Ie) is Relation-like v \ Ie -defined Ie \/ v -defined Sigma -valued Function-like finite Element of bool [:(Ie \/ v),Sigma:]
rng (E1 | (v \ Ie)) is finite Element of bool Sigma
((rng (E1 | (Ie /\ v))) \/ (rng (E1 | (Ie \ v)))) \/ (rng (E1 | (v \ Ie))) is finite Element of bool Sigma
dom (E1 | (v \ Ie)) is finite Element of bool (Ie \/ v)
bool (Ie \/ v) is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
dom E1 is non empty finite Element of bool (Ie \/ v)
(dom E1) /\ (v \ Ie) is finite Element of bool Omega
(Ie \/ v) /\ (v \ Ie) is finite Element of bool Omega
(Ie \/ v) /\ v is finite Element of bool Omega
((Ie \/ v) /\ v) \ Ie is finite Element of bool Omega
E2 is set
(E1 | (v \ Ie)) . E2 is set
x . E2 is set
E . E2 is set
E1 . E2 is set
v /\ v is finite Element of bool Omega
(v /\ v) \ Ie is finite Element of bool Omega
v /\ (v \ Ie) is finite Element of bool Omega
dom x is non empty finite Element of bool v
bool v is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
(dom x) /\ (v \ Ie) is finite Element of bool Omega
meet (rng (E1 | (v \ Ie))) is set
x | (v \ Ie) is Relation-like v -defined v \ Ie -defined v -defined Sigma -valued Function-like finite Element of bool [:v,Sigma:]
rng (x | (v \ Ie)) is finite Element of bool Sigma
meet (rng (x | (v \ Ie))) is set
dom (E1 | (Ie \ v)) is finite Element of bool (Ie \/ v)
(dom E1) /\ (Ie \ v) is finite Element of bool Omega
(Ie \/ v) /\ (Ie \ v) is finite Element of bool Omega
(Ie \/ v) /\ Ie is finite Element of bool Omega
((Ie \/ v) /\ Ie) \ v is finite Element of bool Omega
E2 is set
(E1 | (Ie \ v)) . E2 is set
u . E2 is set
E1 . E2 is set
E . E2 is set
Ie /\ Ie is finite Element of bool Omega
(Ie /\ Ie) \ v is finite Element of bool Omega
Ie /\ (Ie \ v) is finite Element of bool Omega
dom u is non empty finite Element of bool Ie
bool Ie is non empty finite V52() cup-closed intersection_stable diff-closed preBoolean set
(dom u) /\ (Ie \ v) is finite Element of bool Omega
meet (rng (E1 | (Ie \ v))) is set
u | (Ie \ v) is Relation-like Ie -defined Ie \ v -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
rng (u | (Ie \ v)) is finite Element of bool Sigma
meet (rng (u | (Ie \ v))) is set
(meet (rng u)) /\ (meet (rng x)) is set
u | Ie is Relation-like Ie -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
v \/ Ie is non empty finite Element of bool Omega
(meet (rng (E1 | (Ie /\ v)))) /\ (meet (rng (E1 | (v \ Ie)))) is set
(meet (rng u)) /\ (meet (rng (x | (Ie /\ v)))) is set
((meet (rng u)) /\ (meet (rng (x | (Ie /\ v))))) /\ (meet (rng (x | (v \ Ie)))) is set
x | (Ie \ v) is Relation-like v -defined Ie \ v -defined v -defined Sigma -valued Function-like finite Element of bool [:v,Sigma:]
rng (x | (Ie \ v)) is finite Element of bool Sigma
(rng (x | (Ie /\ v))) \/ (rng (x | (Ie \ v))) is finite Element of bool Sigma
((rng (x | (Ie /\ v))) \/ (rng (x | (Ie \ v)))) \/ (rng (x | (v \ Ie))) is finite Element of bool Sigma
(rng (x | (Ie /\ v))) \/ (rng (x | (v \ Ie))) is finite Element of bool Sigma
(meet (rng (x | (Ie /\ v)))) /\ (meet (rng (x | (v \ Ie)))) is set
u | (v \ Ie) is Relation-like Ie -defined v \ Ie -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
rng (u | (v \ Ie)) is finite Element of bool Sigma
(rng (u | (Ie /\ v))) \/ (rng (u | (Ie \ v))) is finite Element of bool Sigma
((rng (u | (Ie /\ v))) \/ (rng (u | (Ie \ v)))) \/ (rng (u | (v \ Ie))) is finite Element of bool Sigma
(meet (rng (E1 | (Ie /\ v)))) /\ (meet (rng (E1 | (Ie \ v)))) is set
(meet (rng (u | (Ie /\ v)))) /\ (meet (rng (u | (Ie \ v)))) is set
((meet (rng (u | (Ie /\ v)))) /\ (meet (rng (u | (Ie \ v))))) /\ (meet (rng (x | (Ie /\ v)))) is set
meet ((rng (E1 | (Ie /\ v))) \/ (rng (E1 | (Ie \ v)))) is set
(meet ((rng (E1 | (Ie /\ v))) \/ (rng (E1 | (Ie \ v))))) /\ (meet (rng (E1 | (v \ Ie)))) is set
(meet (rng (E1 | (Ie /\ v)))) /\ (meet (rng (E1 | (Ie \ v)))) is set
((meet (rng (E1 | (Ie /\ v)))) /\ (meet (rng (E1 | (Ie \ v))))) /\ (meet (rng (E1 | (v \ Ie)))) is set
(meet (rng (u | (Ie /\ v)))) /\ (meet (rng (u | (Ie \ v)))) is set
((meet (rng (u | (Ie /\ v)))) /\ (meet (rng (u | (Ie \ v))))) /\ (meet (rng (x | (Ie /\ v)))) is set
(((meet (rng (u | (Ie /\ v)))) /\ (meet (rng (u | (Ie \ v))))) /\ (meet (rng (x | (Ie /\ v))))) /\ (meet (rng (x | (v \ Ie)))) is set
Ie \/ (Ie /\ v) is non empty finite Element of bool Omega
Ie /\ (Ie /\ v) is finite Element of bool Omega
u | (Ie /\ (Ie /\ v)) is Relation-like Ie -defined Ie /\ (Ie /\ v) -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
rng (u | (Ie /\ (Ie /\ v))) is finite Element of bool Sigma
Ie \ (Ie /\ v) is finite Element of bool Omega
u | (Ie \ (Ie /\ v)) is Relation-like Ie -defined Ie \ (Ie /\ v) -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
rng (u | (Ie \ (Ie /\ v))) is finite Element of bool Sigma
(rng (u | (Ie /\ (Ie /\ v)))) \/ (rng (u | (Ie \ (Ie /\ v)))) is finite Element of bool Sigma
(Ie /\ v) \ Ie is finite Element of bool Omega
u | ((Ie /\ v) \ Ie) is Relation-like Ie -defined (Ie /\ v) \ Ie -defined Ie -defined Sigma -valued Function-like finite Element of bool [:Ie,Sigma:]
rng (u | ((Ie /\ v) \ Ie)) is finite Element of bool Sigma
((rng (u | (Ie /\ (Ie /\ v)))) \/ (rng (u | (Ie \ (Ie /\ v))))) \/ (rng (u | ((Ie /\ v) \ Ie))) is finite Element of bool Sigma
v \ (Ie /\ v) is finite Element of bool Omega
(Ie /\ v) \ v is finite Element of bool Omega
v \/ (Ie /\ v) is non empty finite Element of bool Omega
v /\ (Ie /\ v) is finite Element of bool Omega
(v /\ v) /\ Ie is finite Element of bool Omega
(rng (x | (Ie /\ v))) \/ (rng (x | (v \ Ie))) is finite Element of bool Sigma
x | {} is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined {} -defined v -defined RAT -valued Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:v,Sigma:]
rng (x | {}) is ext-real empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool REAL
((rng (x | (Ie /\ v))) \/ (rng (x | (v \ Ie)))) \/ (rng (x | {})) is finite set
(meet (rng (x | (Ie /\ v)))) /\ (meet (rng (x | (v \ Ie)))) is set
(Ie /\ Ie) /\ v is finite Element of bool Omega
(rng (u | (Ie /\ v))) \/ (rng (u | (Ie \ v))) is finite Element of bool Sigma
(meet (rng u)) /\ (meet (rng x)) is set
E2 is set
E3 is set
X is set
E3 /\ X is set
E2 is Element of bool I
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is non empty Relation-like Sigma -defined REAL -valued Function-like V26(Sigma) V30(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
a is non empty Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
F is non empty Element of bool Omega
T is non empty Element of bool Omega
(Omega,I,Sigma,a,F) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,a,F) is non empty Relation-like F -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(F) V30(F, bool Sigma) Element of bool [:F,(bool Sigma):]
[:F,(bool Sigma):] is non empty Relation-like set
bool [:F,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,F,I,Sigma,(Omega,I,Sigma,a,F)) is Element of bool (bool I)
rng (Omega,I,Sigma,a,F) is non empty set
union (rng (Omega,I,Sigma,a,F)) is set
sigma (Omega,F,I,Sigma,(Omega,I,Sigma,a,F)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,a,T) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,a,T) is non empty Relation-like T -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(T) V30(T, bool Sigma) Element of bool [:T,(bool Sigma):]
[:T,(bool Sigma):] is non empty Relation-like set
bool [:T,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,T,I,Sigma,(Omega,I,Sigma,a,T)) is Element of bool (bool I)
rng (Omega,I,Sigma,a,T) is non empty set
union (rng (Omega,I,Sigma,a,T)) is set
sigma (Omega,T,I,Sigma,(Omega,I,Sigma,a,T)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(I,Sigma,Omega,F,a) is intersection_stable Element of bool (bool I)
(I,Sigma,Omega,T,a) is intersection_stable Element of bool (bool I)
Ie is Event of Sigma
u is Event of Sigma
v is Element of bool I
x is Element of bool I
v /\ x is Element of bool I
P . (v /\ x) is ext-real V14() real set
P . v is ext-real V14() real set
P . x is ext-real V14() real set
(P . v) * (P . x) is ext-real V14() real set
Ie is Event of Sigma
P . Ie is ext-real V14() real Element of REAL
u is Event of Sigma
Ie /\ u is Event of Sigma
P . (Ie /\ u) is ext-real V14() real Element of REAL
P . u is ext-real V14() real Element of REAL
(P . Ie) * (P . u) is ext-real V14() real set
sigma (I,Sigma,Omega,F,a) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
sigma (I,Sigma,Omega,T,a) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Omega is set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
P is Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
a is set
F is set
F is Element of bool (bool I)
T is Element of bool I
Ie is finite Element of bool Omega
(Omega,I,Sigma,P,Ie) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,Ie) is Relation-like Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Ie) V30(Ie, bool Sigma) finite Element of bool [:Ie,(bool Sigma):]
[:Ie,(bool Sigma):] is Relation-like set
bool [:Ie,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,Ie,I,Sigma,(Omega,I,Sigma,P,Ie)) is Element of bool (bool I)
rng (Omega,I,Sigma,P,Ie) is finite set
union (rng (Omega,I,Sigma,P,Ie)) is set
sigma (Omega,Ie,I,Sigma,(Omega,I,Sigma,P,Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
a is Element of bool (bool I)
F is Element of bool (bool I)
T is Element of bool I
Ie is finite Element of bool Omega
(Omega,I,Sigma,P,Ie) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,Ie) is Relation-like Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Ie) V30(Ie, bool Sigma) finite Element of bool [:Ie,(bool Sigma):]
[:Ie,(bool Sigma):] is Relation-like set
bool [:Ie,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,Ie,I,Sigma,(Omega,I,Sigma,P,Ie)) is Element of bool (bool I)
rng (Omega,I,Sigma,P,Ie) is finite set
union (rng (Omega,I,Sigma,P,Ie)) is set
sigma (Omega,Ie,I,Sigma,(Omega,I,Sigma,P,Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
Ie is finite Element of bool Omega
(Omega,I,Sigma,P,Ie) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,Ie) is Relation-like Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Ie) V30(Ie, bool Sigma) finite Element of bool [:Ie,(bool Sigma):]
[:Ie,(bool Sigma):] is Relation-like set
bool [:Ie,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,Ie,I,Sigma,(Omega,I,Sigma,P,Ie)) is Element of bool (bool I)
rng (Omega,I,Sigma,P,Ie) is finite set
union (rng (Omega,I,Sigma,P,Ie)) is set
sigma (Omega,Ie,I,Sigma,(Omega,I,Sigma,P,Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
Omega is non empty set
I is non empty set
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is non empty Relation-like Omega -defined bool Sigma -valued Function-like V26(Omega) V30(Omega, bool Sigma) (Omega,I,Sigma)
(Omega,I,Sigma,P) is non empty Element of bool (bool I)
bool I is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool I)
(Omega,I,Sigma,P) is non empty Element of bool (bool (bool I))
bool (bool I) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool I)) is non empty cup-closed intersection_stable diff-closed preBoolean set
meet (Omega,I,Sigma,P) is Element of bool (bool I)
[:NAT,(bool I):] is non empty Relation-like set
bool [:NAT,(bool I):] is non empty cup-closed intersection_stable diff-closed preBoolean set
a is non empty Relation-like NAT -defined bool I -valued Function-like V26( NAT ) V30( NAT , bool I) Element of bool [:NAT,(bool I):]
rng a is non empty Element of bool (bool I)
Intersection a is Element of bool I
Complement a is non empty Relation-like NAT -defined bool I -valued Function-like V26( NAT ) V30( NAT , bool I) Element of bool [:NAT,(bool I):]
Union (Complement a) is Element of bool I
rng (Complement a) is non empty set
union (rng (Complement a)) is set
(Union (Complement a)) ` is Element of bool I
I \ (Union (Complement a)) is set
F is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
a . F is Event of bool I
T is set
F is set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
Ie is finite Element of bool Omega
Omega \ Ie is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ Ie)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ Ie)) is Relation-like Omega \ Ie -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ Ie) V30(Omega \ Ie, bool Sigma) Element of bool [:(Omega \ Ie),(bool Sigma):]
[:(Omega \ Ie),(bool Sigma):] is Relation-like set
bool [:(Omega \ Ie),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ Ie)) is set
union (rng (Omega,I,Sigma,P,(Omega \ Ie))) is set
sigma (Omega,(Omega \ Ie),I,Sigma,(Omega,I,Sigma,P,(Omega \ Ie))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
T is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
Ie is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real set
(Complement a) . Ie is set
u is ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V77() V78() V79() V80() V81() V82() V83() V84() Element of NAT
a . u is Event of bool I
(a . u) ` is Element of bool I
I \ (a . u) is set
rng (Complement a) is non empty Element of bool (bool I)
Ie is non empty Relation-like NAT -defined bool I -valued T -valued Function-like V26( NAT ) V30( NAT , bool I) Element of bool [:NAT,(bool I):]
Union Ie is Element of bool I
rng Ie is non empty set
union (rng Ie) is set
a is Element of bool I
a ` is Element of bool I
I \ a is set
F is set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
T is finite Element of bool Omega
Omega \ T is Element of bool Omega
(Omega,I,Sigma,P,(Omega \ T)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
(Omega,I,Sigma,P,(Omega \ T)) is Relation-like Omega \ T -defined Omega -defined bool Sigma -valued bool Sigma -valued Function-like V26(Omega \ T) V30(Omega \ T, bool Sigma) Element of bool [:(Omega \ T),(bool Sigma):]
[:(Omega \ T),(bool Sigma):] is Relation-like set
bool [:(Omega \ T),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(Omega,(Omega \ T),I,Sigma,(Omega,I,Sigma,P,(Omega \ T))) is Element of bool (bool I)
rng (Omega,I,Sigma,P,(Omega \ T)) is set
union (rng (Omega,I,Sigma,P,(Omega \ T))) is set
sigma (Omega,(Omega \ T),I,Sigma,(Omega,I,Sigma,P,(Omega \ T))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool I)
Omega is non empty set
bool Omega is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
I is non empty set
Sigma is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
bool Sigma is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Sigma)
bool Sigma is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
P is non empty Relation-like Sigma -defined REAL -valued Function-like V26(Sigma) V30(Sigma, REAL ) V33() V34() V35() V42() Probability of Sigma
a is Element of Sigma
P . a is ext-real V14() real Element of REAL
F is non empty Relation-like I -defined bool Sigma -valued Function-like V26(I) V30(I, bool Sigma) (I,Omega,Sigma)
(I,Omega,Sigma,F) is non empty Element of bool (bool Omega)
bool Omega is non empty compl-closed sigma-multiplicative cup-closed intersection_stable diff-closed preBoolean Element of bool (bool Omega)
(I,Omega,Sigma,F) is non empty Element of bool (bool (bool Omega))
bool (bool Omega) is non empty cup-closed intersection_stable diff-closed preBoolean set
bool (bool (bool Omega)) is non empty cup-closed intersection_stable diff-closed preBoolean set
meet (I,Omega,Sigma,F) is Element of bool (bool Omega)
{} I is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool I
bool I is non empty cup-closed intersection_stable diff-closed preBoolean set
I \ ({} I) is Element of bool I
(I,Omega,Sigma,F,(I \ ({} I))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,(I \ ({} I))) is Relation-like I \ ({} I) -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(I \ ({} I)) V30(I \ ({} I), bool Sigma) Element of bool [:(I \ ({} I)),(bool Sigma):]
[:(I \ ({} I)),(bool Sigma):] is Relation-like set
bool [:(I \ ({} I)),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,(I \ ({} I)),Omega,Sigma,(I,Omega,Sigma,F,(I \ ({} I)))) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,(I \ ({} I))) is set
union (rng (I,Omega,Sigma,F,(I \ ({} I)))) is set
sigma (I,(I \ ({} I)),Omega,Sigma,(I,Omega,Sigma,F,(I \ ({} I)))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
u is finite Element of bool I
(I,Omega,Sigma,F,u) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,u) is Relation-like u -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(u) V30(u, bool Sigma) finite Element of bool [:u,(bool Sigma):]
[:u,(bool Sigma):] is Relation-like set
bool [:u,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,u,Omega,Sigma,(I,Omega,Sigma,F,u)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,u) is finite set
union (rng (I,Omega,Sigma,F,u)) is set
sigma (I,u,Omega,Sigma,(I,Omega,Sigma,F,u)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
v is Event of Sigma
x is Event of Sigma
E is finite Element of bool I
I \ E is Element of bool I
(I,Omega,Sigma,F,(I \ E)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,(I \ E)) is Relation-like I \ E -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(I \ E) V30(I \ E, bool Sigma) Element of bool [:(I \ E),(bool Sigma):]
[:(I \ E),(bool Sigma):] is Relation-like set
bool [:(I \ E),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,(I \ E),Omega,Sigma,(I,Omega,Sigma,F,(I \ E))) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,(I \ E)) is set
union (rng (I,Omega,Sigma,F,(I \ E))) is set
sigma (I,(I \ E),Omega,Sigma,(I,Omega,Sigma,F,(I \ E))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
I \ u is Element of bool I
(I,Omega,Sigma,F,(I \ u)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,(I \ u)) is Relation-like I \ u -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(I \ u) V30(I \ u, bool Sigma) Element of bool [:(I \ u),(bool Sigma):]
[:(I \ u),(bool Sigma):] is Relation-like set
bool [:(I \ u),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,(I \ u),Omega,Sigma,(I,Omega,Sigma,F,(I \ u))) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,(I \ u)) is set
union (rng (I,Omega,Sigma,F,(I \ u))) is set
sigma (I,(I \ u),Omega,Sigma,(I,Omega,Sigma,F,(I \ u))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
E is non empty Element of bool I
I \ E is Element of bool I
y is non empty Element of bool I
v /\ x is Event of Sigma
P . (v /\ x) is ext-real V14() real Element of REAL
P . v is ext-real V14() real Element of REAL
P . x is ext-real V14() real Element of REAL
(P . v) * (P . x) is ext-real V14() real set
{{},Omega} is non empty finite intersection_stable set
y is Event of Sigma
E1 is Event of Sigma
[#] Sigma is Event of Sigma
F | {} is ext-real empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined {} -defined I -defined RAT -valued bool Sigma -valued Function-like one-to-one constant functional V33() V34() V35() V36() finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() Element of bool [:I,(bool Sigma):]
[:I,(bool Sigma):] is non empty Relation-like set
bool [:I,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
Union (F | {}) is set
rng (F | {}) is ext-real empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() V36() V37() V38() V39() V40() with_non-empty_elements finite finite-yielding V52() FinSequence-like FinSubsequence-like FinSequence-membered V79() V80() V81() V82() V83() V84() V85() set
union (rng (F | {})) is epsilon-transitive epsilon-connected ordinal finite set
E is Element of bool I
(I,Omega,Sigma,F,E) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,E) is Relation-like E -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(E) V30(E, bool Sigma) Element of bool [:E,(bool Sigma):]
[:E,(bool Sigma):] is Relation-like set
bool [:E,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,E,Omega,Sigma,(I,Omega,Sigma,F,E)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,E) is set
union (rng (I,Omega,Sigma,F,E)) is set
sigma (I,E,Omega,Sigma,(I,Omega,Sigma,F,E)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F) is Element of bool (bool Omega)
u is Event of Sigma
v is Event of Sigma
x is finite Element of bool I
(I,Omega,Sigma,F,x) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,x) is Relation-like x -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(x) V30(x, bool Sigma) finite Element of bool [:x,(bool Sigma):]
[:x,(bool Sigma):] is Relation-like set
bool [:x,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,x,Omega,Sigma,(I,Omega,Sigma,F,x)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,x) is finite set
union (rng (I,Omega,Sigma,F,x)) is set
sigma (I,x,Omega,Sigma,(I,Omega,Sigma,F,x)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
sigma (I,Omega,Sigma,F) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
u is set
dom F is non empty Element of bool I
rng F is non empty Element of bool (bool Sigma)
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
union (rng F) is Element of bool Sigma
v is set
x is set
F . x is Element of bool (bool Omega)
E is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
sigma E is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
{x} is non empty finite set
y is set
F | {x} is Relation-like I -defined {x} -defined I -defined bool Sigma -valued Function-like finite Element of bool [:I,(bool Sigma):]
[:I,(bool Sigma):] is non empty Relation-like set
bool [:I,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
dom (F | {x}) is finite Element of bool I
(dom F) /\ {x} is finite Element of bool I
rng (F | {x}) is finite Element of bool (bool Sigma)
(F | {x}) . x is set
{((F | {x}) . x)} is non empty finite set
union (rng (F | {x})) is Element of bool Sigma
Union (F | {x}) is set
rng (F | {x}) is finite set
union (rng (F | {x})) is set
y is finite Element of bool I
(I,Omega,Sigma,F,y) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,y) is Relation-like y -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(y) V30(y, bool Sigma) finite Element of bool [:y,(bool Sigma):]
[:y,(bool Sigma):] is Relation-like set
bool [:y,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,y,Omega,Sigma,(I,Omega,Sigma,F,y)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,y) is finite set
union (rng (I,Omega,Sigma,F,y)) is set
sigma (I,y,Omega,Sigma,(I,Omega,Sigma,F,y)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
T is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
sigma T is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
u is set
v is set
u /\ v is set
x is finite Element of bool I
(I,Omega,Sigma,F,x) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,x) is Relation-like x -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(x) V30(x, bool Sigma) finite Element of bool [:x,(bool Sigma):]
[:x,(bool Sigma):] is Relation-like set
bool [:x,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,x,Omega,Sigma,(I,Omega,Sigma,F,x)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,x) is finite set
union (rng (I,Omega,Sigma,F,x)) is set
sigma (I,x,Omega,Sigma,(I,Omega,Sigma,F,x)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
E is finite Element of bool I
(I,Omega,Sigma,F,E) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,E) is Relation-like E -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(E) V30(E, bool Sigma) finite Element of bool [:E,(bool Sigma):]
[:E,(bool Sigma):] is Relation-like set
bool [:E,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,E,Omega,Sigma,(I,Omega,Sigma,F,E)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,E) is finite set
union (rng (I,Omega,Sigma,F,E)) is set
sigma (I,E,Omega,Sigma,(I,Omega,Sigma,F,E)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
y is set
E1 is finite Element of bool I
(I,Omega,Sigma,F,E1) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,E1) is Relation-like E1 -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(E1) V30(E1, bool Sigma) finite Element of bool [:E1,(bool Sigma):]
[:E1,(bool Sigma):] is Relation-like set
bool [:E1,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,E1,Omega,Sigma,(I,Omega,Sigma,F,E1)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,E1) is finite set
union (rng (I,Omega,Sigma,F,E1)) is set
sigma (I,E1,Omega,Sigma,(I,Omega,Sigma,F,E1)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
E2 is finite Element of bool I
E1 \/ E2 is finite Element of bool I
(I,Omega,Sigma,F,(E1 \/ E2)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,(E1 \/ E2)) is Relation-like E1 \/ E2 -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(E1 \/ E2) V30(E1 \/ E2, bool Sigma) finite Element of bool [:(E1 \/ E2),(bool Sigma):]
[:(E1 \/ E2),(bool Sigma):] is Relation-like set
bool [:(E1 \/ E2),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,(E1 \/ E2),Omega,Sigma,(I,Omega,Sigma,F,(E1 \/ E2))) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,(E1 \/ E2)) is finite set
union (rng (I,Omega,Sigma,F,(E1 \/ E2))) is set
sigma (I,(E1 \/ E2),Omega,Sigma,(I,Omega,Sigma,F,(E1 \/ E2))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
E3 is finite Element of bool I
(I,Omega,Sigma,F,E3) is Relation-like E3 -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(E3) V30(E3, bool Sigma) finite Element of bool [:E3,(bool Sigma):]
[:E3,(bool Sigma):] is Relation-like set
bool [:E3,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,E3,Omega,Sigma,(I,Omega,Sigma,F,E3)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,E3) is finite set
union (rng (I,Omega,Sigma,F,E3)) is set
X is set
rng (I,Omega,Sigma,F,E1) is finite Element of bool (bool Sigma)
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
S is set
(I,Omega,Sigma,F,E2) is Relation-like E2 -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(E2) V30(E2, bool Sigma) finite Element of bool [:E2,(bool Sigma):]
[:E2,(bool Sigma):] is Relation-like set
bool [:E2,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,Omega,Sigma,F,E1) \/ (I,Omega,Sigma,F,E2) is Relation-like I -defined bool Sigma -valued finite set
rng (I,Omega,Sigma,F,E3) is finite Element of bool (bool Sigma)
rng (I,Omega,Sigma,F,E2) is finite Element of bool (bool Sigma)
(rng (I,Omega,Sigma,F,E1)) \/ (rng (I,Omega,Sigma,F,E2)) is finite Element of bool (bool Sigma)
sigma (I,E3,Omega,Sigma,(I,Omega,Sigma,F,E3)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
E \/ x is finite Element of bool I
(I,Omega,Sigma,F,(E \/ x)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,(E \/ x)) is Relation-like E \/ x -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(E \/ x) V30(E \/ x, bool Sigma) finite Element of bool [:(E \/ x),(bool Sigma):]
[:(E \/ x),(bool Sigma):] is Relation-like set
bool [:(E \/ x),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,(E \/ x),Omega,Sigma,(I,Omega,Sigma,F,(E \/ x))) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,(E \/ x)) is finite set
union (rng (I,Omega,Sigma,F,(E \/ x))) is set
sigma (I,(E \/ x),Omega,Sigma,(I,Omega,Sigma,F,(E \/ x))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
x \/ E is finite Element of bool I
(I,Omega,Sigma,F,(x \/ E)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,(x \/ E)) is Relation-like x \/ E -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(x \/ E) V30(x \/ E, bool Sigma) finite Element of bool [:(x \/ E),(bool Sigma):]
[:(x \/ E),(bool Sigma):] is Relation-like set
bool [:(x \/ E),(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,(x \/ E),Omega,Sigma,(I,Omega,Sigma,F,(x \/ E))) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,(x \/ E)) is finite set
union (rng (I,Omega,Sigma,F,(x \/ E))) is set
sigma (I,(x \/ E),Omega,Sigma,(I,Omega,Sigma,F,(x \/ E))) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
u is Event of Sigma
v is Event of Sigma
the finite Element of bool I is finite Element of bool I
(I,Omega,Sigma,F, the finite Element of bool I) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F, the finite Element of bool I) is Relation-like the finite Element of bool I -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26( the finite Element of bool I) V30( the finite Element of bool I, bool Sigma) finite Element of bool [: the finite Element of bool I,(bool Sigma):]
[: the finite Element of bool I,(bool Sigma):] is Relation-like set
bool [: the finite Element of bool I,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I, the finite Element of bool I,Omega,Sigma,(I,Omega,Sigma,F, the finite Element of bool I)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F, the finite Element of bool I) is finite set
union (rng (I,Omega,Sigma,F, the finite Element of bool I)) is set
sigma (I, the finite Element of bool I,Omega,Sigma,(I,Omega,Sigma,F, the finite Element of bool I)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
E is set
y is set
rng (I,Omega,Sigma,F,(I \ ({} I))) is Element of bool (bool Sigma)
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
E1 is set
x is set
E is finite Element of bool I
(I,Omega,Sigma,F,E) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
(I,Omega,Sigma,F,E) is Relation-like E -defined I -defined bool Sigma -valued bool Sigma -valued Function-like V26(E) V30(E, bool Sigma) finite Element of bool [:E,(bool Sigma):]
[:E,(bool Sigma):] is Relation-like set
bool [:E,(bool Sigma):] is non empty cup-closed intersection_stable diff-closed preBoolean set
(I,E,Omega,Sigma,(I,Omega,Sigma,F,E)) is Element of bool (bool Omega)
rng (I,Omega,Sigma,F,E) is finite set
union (rng (I,Omega,Sigma,F,E)) is set
sigma (I,E,Omega,Sigma,(I,Omega,Sigma,F,E)) is non empty compl-closed sigma-multiplicative intersection_stable Element of bool (bool Omega)
y is set
rng (I,Omega,Sigma,F,E) is finite Element of bool (bool Sigma)
bool (bool Sigma) is non empty cup-closed intersection_stable diff-closed preBoolean set
E1 is set
a /\ a is Event of Sigma
P . (a /\ a) is ext-real V14() real Element of REAL
(P . a) * (P . a) is ext-real V14() real set