REAL is set
NAT is non empty V7() V8() V9() Element of bool REAL
bool REAL is non empty V59() set
NAT is non empty V7() V8() V9() set
bool NAT is non empty V59() set
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is non empty V59() set
bool (bool REAL) is non empty V59() set
0 is empty V7() V8() V9() V11() V12() V13() V14() ext-real Relation-like non-empty empty-yielding V57() set
0 is empty V7() V8() V9() V11() V12() V13() V14() ext-real Relation-like non-empty empty-yielding V57() Element of NAT
1 is non empty V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + Si is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S is set
[:NAT,S:] is Relation-like set
bool [:NAT,S:] is non empty V59() set
S is Relation-like NAT -defined S -valued Function-like V32( NAT ,S) Element of bool [:NAT,S:]
S . (X + Si) is Element of S
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
[:NAT,Si:] is Relation-like set
bool [:NAT,Si:] is non empty V59() set
S is Relation-like NAT -defined Si -valued Function-like V32( NAT ,Si) Element of bool [:NAT,Si:]
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X + 1 <= b1 } is set
S . X is Element of Si
{(S . X)} is non empty set
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X + 1 <= b1 } \/ {(S . X)} is non empty set
A3 is set
B is set
A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . A2 is Element of Si
A3 is set
B is set
A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . A2 is Element of Si
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
[:NAT,Si:] is Relation-like set
bool [:NAT,Si:] is non empty V59() set
S is set
S is Relation-like NAT -defined Si -valued Function-like V32( NAT ,Si) Element of bool [:NAT,Si:]
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
A3 is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of Si
A2 is V7() V8() V9() V13() V14() ext-real V57() set
X + A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
A2 is V7() V8() V9() V13() V14() ext-real V57() set
X + A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A2) is Element of Si
A3 is set
A3 is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + B) is Element of Si
A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A2) is Element of Si
X is set
Si is non empty set
[:NAT,Si:] is non empty Relation-like set
bool [:NAT,Si:] is non empty V59() set
S is non empty Relation-like NAT -defined Si -valued Function-like V28( NAT ) V32( NAT ,Si) Element of bool [:NAT,Si:]
rng S is non empty Element of bool Si
bool Si is non empty V59() set
dom S is non empty Element of bool NAT
bool NAT is non empty V59() set
S is set
S . S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of Si
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . S is Element of Si
dom S is non empty Element of bool NAT
bool NAT is non empty V59() set
X is non empty set
[:NAT,X:] is non empty Relation-like set
bool [:NAT,X:] is non empty V59() set
Si is non empty Relation-like NAT -defined X -valued Function-like V28( NAT ) V32( NAT ,X) Element of bool [:NAT,X:]
rng Si is non empty Element of bool X
bool X is non empty V59() set
{ (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : 0 <= b1 } is set
dom Si is non empty Element of bool NAT
bool NAT is non empty V59() set
S is set
B is set
Si . B is set
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . B is Element of X
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is non empty set
[:NAT,Si:] is non empty Relation-like set
bool [:NAT,Si:] is non empty V59() set
S is non empty Relation-like NAT -defined Si -valued Function-like V28( NAT ) V32( NAT ,Si) Element of bool [:NAT,Si:]
S ^\ X is non empty Relation-like NAT -defined Si -valued Function-like V28( NAT ) V32( NAT ,Si) Element of bool [:NAT,Si:]
rng (S ^\ X) is non empty Element of bool Si
bool Si is non empty V59() set
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
S is non empty Relation-like NAT -defined Si -valued Function-like V28( NAT ) V32( NAT ,Si) Element of bool [:NAT,Si:]
rng S is non empty Element of bool Si
dom S is non empty Element of bool NAT
bool NAT is non empty V59() set
A3 is set
B is set
S . B is set
A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A2) is Element of Si
A3 is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of Si
A2 is V7() V8() V9() V13() V14() ext-real V57() set
X + A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . A2 is set
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is set
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
rng S is non empty Element of bool (bool X)
bool (bool X) is non empty V59() set
meet (rng S) is Element of bool X
dom S is non empty Element of bool NAT
bool NAT is non empty V59() set
S is set
B is set
A3 is set
S . A3 is set
S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool X
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool X
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . S is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Intersection Si is Element of bool X
rng Si is non empty Element of bool (bool X)
bool (bool X) is non empty V59() set
meet (rng Si) is Element of bool X
S is set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . S is Element of bool X
S is set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . S is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Intersection Si is Element of bool X
Union Si is Element of bool X
rng Si is non empty Element of bool (bool X)
bool (bool X) is non empty V59() set
meet (rng Si) is Element of bool X
union (rng Si) is Element of bool X
X is set
bool X is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Union S is Element of bool X
S is set
rng S is non empty Element of bool (bool X)
bool (bool X) is non empty V59() set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool X
{Si} is non empty set
union (rng S) is Element of bool X
X is set
bool X is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Intersection S is Element of bool X
S is set
rng S is non empty Element of bool (bool X)
bool (bool X) is non empty V59() set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool X
{Si} is non empty set
meet (rng S) is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Union Si is Element of bool X
Intersection Si is Element of bool X
S is Element of bool X
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . S is Element of bool X
X is set
bool X is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
the_value_of S is set
Union S is Element of bool X
Intersection S is Element of bool X
dom S is non empty Element of bool NAT
bool NAT is non empty V59() set
S is set
S . S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool X
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool X
X is set
bool X is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
the_value_of S is set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
union { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
A3 is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool X
{Si} is non empty set
X is set
bool X is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
the_value_of S is set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
meet { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
A3 is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool X
{Si} is non empty set
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
S is Relation-like Function-like set
dom S is set
rng S is set
S is set
B is set
S . B is set
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : A3 <= b1 } is set
meet { (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : A3 <= b1 } is set
X1 is set
x is set
k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . k is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
S is Relation-like Function-like set
dom S is set
rng S is set
S is set
B is set
S . B is set
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : A3 <= b1 } is set
union { (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : A3 <= b1 } is set
X1 is set
x is set
x is set
k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . k is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
X is Relation-like Function-like set
{ (X . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : a1 <= b1 } is set
meet { (X . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : a1 <= b1 } is set
Si is Relation-like Function-like set
dom Si is set
S is Relation-like Function-like set
dom S is set
S is set
Si . S is set
S . S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (X . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : B <= b1 } is set
Si . B is set
meet { (X . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : B <= b1 } is set
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(Si) is Relation-like Function-like set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Si) . S is set
{ (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
meet { (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
dom (Si) is set
X is Relation-like Function-like set
{ (X . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : a1 <= b1 } is set
union { (X . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : a1 <= b1 } is set
Si is Relation-like Function-like set
dom Si is set
S is Relation-like Function-like set
dom S is set
S is set
Si . S is set
S . S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (X . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : B <= b1 } is set
Si . B is set
union { (X . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : B <= b1 } is set
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(Si) is Relation-like Function-like set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Si) . S is set
{ (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
union { (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
dom (Si) is set
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) . 0 is Element of bool X
Intersection Si is Element of bool X
{ (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : 0 <= b1 } is set
meet { (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : 0 <= b1 } is set
rng Si is non empty Element of bool (bool X)
bool (bool X) is non empty V59() set
meet (rng Si) is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) . 0 is Element of bool X
Union Si is Element of bool X
{ (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : 0 <= b1 } is set
union { (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : 0 <= b1 } is set
rng Si is non empty Element of bool (bool X)
bool (bool X) is non empty V59() set
union (rng Si) is Element of bool X
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
meet { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A3) is Element of bool Si
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A3) is Element of bool Si
A3 is set
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A3) is Element of bool Si
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + B) is Element of bool Si
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
union { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
A3 is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool Si
A2 is V7() V8() V9() V13() V14() ext-real V57() set
X + A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
A2 is V7() V8() V9() V13() V14() ext-real V57() set
X + A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A2) is Element of bool Si
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A3) is Element of bool Si
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A3) is Element of bool Si
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (X + A3) is Element of bool Si
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
(Si,S) . (X + 1) is Element of bool Si
S . X is Element of bool Si
((Si,S) . (X + 1)) /\ (S . X) is M7(Si, bool Si)
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Si,S) . S is Element of bool Si
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
meet { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
S + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S + 1 <= b1 } is set
S . S is Element of bool Si
{(S . S)} is non empty set
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S + 1 <= b1 } \/ {(S . S)} is non empty set
(Si,S) . (S + 1) is Element of bool Si
meet { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S + 1 <= b1 } is set
B is set
A3 is set
B is set
A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . A2 is Element of bool Si
B is set
((Si,S) . (S + 1)) /\ (S . S) is M7(Si, bool Si)
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
(Si,S) . (X + 1) is Element of bool Si
S . X is Element of bool Si
((Si,S) . (X + 1)) \/ (S . X) is M7(Si, bool Si)
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
S + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S + 1 <= b1 } is set
S . S is Element of bool Si
{(S . S)} is non empty set
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S + 1 <= b1 } \/ {(S . S)} is non empty set
union { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S + 1 <= b1 } is set
union { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
(Si,S) . (S + 1) is Element of bool Si
(Si,S) . S is Element of bool Si
B is set
B is set
A3 is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool Si
B is set
A3 is set
((Si,S) . (S + 1)) \/ (S . S) is M7(Si, bool Si)
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . S is Element of bool X
S + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . (S + 1) is Element of bool X
Si . S is Element of bool X
((X,Si) . (S + 1)) /\ (Si . S) is M7(X, bool X)
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . S is Element of bool X
S + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . (S + 1) is Element of bool X
Si . S is Element of bool X
((X,Si) . (S + 1)) \/ (Si . S) is M7(X, bool X)
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
Intersection S is Element of bool Si
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-descending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
(Si,S) . 0 is Element of bool Si
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-ascending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
Union S is Element of bool Si
(Si,S) . 0 is Element of bool Si
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (Si . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
B is set
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . A3 is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Union Si is Element of bool X
Complement Si is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Intersection (Complement Si) is Element of bool X
(Intersection (Complement Si)) ` is Element of bool X
X \ (Intersection (Complement Si)) is set
Complement (Complement Si) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Union (Complement (Complement Si)) is Element of bool X
(Union (Complement (Complement Si))) ` is Element of bool X
X \ (Union (Complement (Complement Si))) is set
((Union (Complement (Complement Si))) `) ` is Element of bool X
X \ ((Union (Complement (Complement Si))) `) is set
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-descending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
Complement S is non empty Relation-like NAT -defined bool Si -valued bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,(Complement S)) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-ascending Element of bool [:NAT,(bool Si):]
(Si,(Complement S)) . X is Element of bool Si
((Si,(Complement S)) . X) ` is Element of bool Si
Si \ ((Si,(Complement S)) . X) is set
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
{ ((Complement S) . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
{ ((S . b1) `) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X <= b1 } is set
B is set
A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . A2 is Element of bool Si
(S . A2) ` is Element of bool Si
Si \ (S . A2) is set
(Complement S) . A2 is Element of bool Si
B is set
A2 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Complement S) . A2 is Element of bool Si
S . A2 is Element of bool Si
(S . A2) ` is Element of bool Si
Si \ (S . A2) is set
B is Element of bool (bool Si)
COMPLEMENT B is Element of bool (bool Si)
A2 is set
X1 is Element of bool Si
X1 ` is Element of bool Si
Si \ X1 is set
x is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . x is Element of bool Si
(S . x) ` is Element of bool Si
Si \ (S . x) is set
A2 is set
X1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . X1 is Element of bool Si
(S . X1) ` is Element of bool Si
Si \ (S . X1) is set
x is Element of bool Si
x ` is Element of bool Si
Si \ x is set
(x `) ` is Element of bool Si
Si \ (x `) is set
union (COMPLEMENT B) is Element of bool Si
[#] Si is non proper Element of bool Si
meet B is Element of bool Si
([#] Si) \ (meet B) is Element of bool Si
(meet B) ` is Element of bool Si
Si \ (meet B) is set
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-ascending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
Complement S is non empty Relation-like NAT -defined bool Si -valued bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,(Complement S)) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-descending Element of bool [:NAT,(bool Si):]
(Si,(Complement S)) . X is Element of bool Si
((Si,(Complement S)) . X) ` is Element of bool Si
Si \ ((Si,(Complement S)) . X) is set
S is Element of bool Si
Complement (Complement S) is non empty Relation-like NAT -defined bool Si -valued bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,(Complement (Complement S))) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-ascending Element of bool [:NAT,(bool Si):]
(Si,(Complement (Complement S))) . X is Element of bool Si
((Si,(Complement (Complement S))) . X) ` is Element of bool Si
Si \ ((Si,(Complement (Complement S))) . X) is set
((Si,S) . X) ` is Element of bool Si
Si \ ((Si,S) . X) is set
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Complement (X,Si) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Complement Si is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(Complement Si)) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool X
(S . B) ` is Element of bool X
X \ (S . B) is set
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
S . B is Element of bool X
(S . B) ` is Element of bool X
X \ (S . B) is set
((S . B) `) ` is Element of bool X
X \ ((S . B) `) is set
Complement S is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(Complement S) . B is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Complement (X,Si) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Complement Si is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(Complement Si)) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Complement S is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Complement (Complement Si) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(Complement (Complement Si))) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,S) . B is Element of bool X
(X,S) . B is Element of bool X
((X,S) . B) \/ ((X,S) . B) is M7(X, bool X)
(X,Si) . B is Element of bool X
X1 is set
x is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + x is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (B + x) is Element of bool X
Si . (B + x) is Element of bool X
S . (B + x) is Element of bool X
(S . (B + x)) \/ (S . (B + x)) is M7(X, bool X)
x is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + x is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (B + x) is Element of bool X
Si . (B + x) is Element of bool X
S . (B + x) is Element of bool X
(S . (B + x)) \/ (S . (B + x)) is M7(X, bool X)
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
(X,S) . B is Element of bool X
(X,S) . B is Element of bool X
((X,S) . B) /\ ((X,S) . B) is M7(X, bool X)
X1 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
X1 . B is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
B . B is Element of bool X
(X1 . B) /\ (B . B) is M7(X, bool X)
A3 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
A3 . B is Element of bool X
x is set
k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (B + k) is Element of bool X
S . (B + k) is Element of bool X
(S . (B + k)) /\ (S . (B + k)) is M7(X, bool X)
Si . (B + k) is Element of bool X
x is set
k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . (B + k) is Element of bool X
S . (B + k) is Element of bool X
S . (B + k) is Element of bool X
(S . (B + k)) /\ (S . (B + k)) is M7(X, bool X)
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
(X,S) . B is Element of bool X
(X,S) . B is Element of bool X
((X,S) . B) \/ ((X,S) . B) is M7(X, bool X)
X1 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
X1 . B is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
B . B is Element of bool X
(X1 . B) \/ (B . B) is M7(X, bool X)
A3 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
A3 . B is Element of bool X
x is set
k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (B + k) is Element of bool X
Si . (B + k) is Element of bool X
S . (B + k) is Element of bool X
(S . (B + k)) \/ (S . (B + k)) is M7(X, bool X)
k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (B + k) is Element of bool X
Si . (B + k) is Element of bool X
S . (B + k) is Element of bool X
(S . (B + k)) \/ (S . (B + k)) is M7(X, bool X)
x is set
k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . (B + k) is Element of bool X
S . (B + k) is Element of bool X
S . (B + k) is Element of bool X
(S . (B + k)) \/ (S . (B + k)) is M7(X, bool X)
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
(X,S) . B is Element of bool X
(X,S) . B is Element of bool X
((X,S) . B) /\ ((X,S) . B) is M7(X, bool X)
A3 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
A3 . B is Element of bool X
X1 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
X1 . B is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
B . B is Element of bool X
(X1 . B) /\ (B . B) is M7(X, bool X)
x is set
k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + k is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . (B + k) is Element of bool X
S . (B + k) is Element of bool X
S . (B + k) is Element of bool X
(S . (B + k)) /\ (S . (B + k)) is M7(X, bool X)
X is set
bool X is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
the_value_of S is set
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,S) . S is Element of bool X
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
meet { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
X is set
bool X is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
the_value_of S is set
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,S) . S is Element of bool X
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
union { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : S <= b1 } is set
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
S . X is Element of bool Si
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-ascending Element of bool [:NAT,(bool Si):]
(Si,S) . (X + 1) is Element of bool Si
S . (X + 1) is Element of bool Si
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X + 1 <= b1 } is set
union { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X + 1 <= b1 } is set
S is set
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-ascending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
(Si,S) . (X + 1) is Element of bool Si
S . X is Element of bool Si
((Si,S) . (X + 1)) \/ (S . X) is M7(Si, bool Si)
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-ascending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
Union S is Element of bool Si
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Si,S) . S is set
S + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Si,S) . (S + 1) is set
(Si,S) . 0 is set
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,Si) is Element of bool X
Union Si is Element of bool X
S is set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . S is Element of bool X
S is set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . S is Element of bool X
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
S . X is Element of bool Si
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-descending Element of bool [:NAT,(bool Si):]
(Si,S) . (X + 1) is Element of bool Si
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X + 1 <= b1 } is set
B is set
A3 is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . B is Element of bool Si
meet { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X + 1 <= b1 } is set
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-descending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
S . X is Element of bool Si
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Si,S) . (X + 1) is Element of bool Si
((Si,S) . (X + 1)) /\ (S . X) is M7(Si, bool Si)
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . S is Element of bool X
Si . S is Element of bool X
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-ascending Element of bool [:NAT,(bool Si):]
(Si,S) . (X + 1) is Element of bool Si
S . X is Element of bool Si
S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X + 1) + B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . ((X + 1) + B) is Element of bool Si
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-ascending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
S . X is Element of bool Si
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Si,S) . (X + 1) is Element of bool Si
((Si,S) . (X + 1)) \/ (S . X) is M7(Si, bool Si)
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . S is Element of bool X
Si . S is Element of bool X
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-descending Element of bool [:NAT,(bool Si):]
(Si,S) . (X + 1) is Element of bool Si
S . X is Element of bool Si
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X + 1 <= b1 } is set
S . (X + 1) is Element of bool Si
B is set
meet { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : X + 1 <= b1 } is set
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-descending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
(Si,S) . (X + 1) is Element of bool Si
S . X is Element of bool Si
((Si,S) . (X + 1)) /\ (S . X) is M7(Si, bool Si)
X is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si is set
bool Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool Si)
bool Si is non empty V59() set
bool (bool Si) is non empty V59() set
[:NAT,(bool Si):] is non empty Relation-like set
bool [:NAT,(bool Si):] is non empty V59() set
S is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) Element of bool [:NAT,(bool Si):]
(Si,S) is non empty Relation-like NAT -defined bool Si -valued Function-like V28( NAT ) V32( NAT , bool Si) non-descending Element of bool [:NAT,(bool Si):]
(Si,S) . X is Element of bool Si
Intersection S is Element of bool Si
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Si,S) . S is set
S + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(Si,S) . (S + 1) is set
(Si,S) . 0 is set
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,Si) is Element of bool X
Intersection Si is Element of bool X
S is set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . S is Element of bool X
S is set
(X,Si) . 0 is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,Si) is Element of bool X
S is Element of bool X
S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . (B + A3) is Element of bool X
S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . (B + A3) is Element of bool X
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,Si) is Element of bool X
S is Element of bool X
S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . (B + A3) is Element of bool X
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,Si) . B is Element of bool X
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . (B + A3) is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Intersection Si is Element of bool X
lim_inf Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,Si) is Element of bool X
S is set
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
0 + S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
Si . (0 + S) is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,Si) is Element of bool X
lim_sup (X,Si) is Element of bool X
(X,(X,Si)) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(X,Si)) is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,Si) is Element of bool X
lim_sup (X,Si) is Element of bool X
(X,(X,Si)) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(X,Si)) is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,Si) is Element of bool X
Complement Si is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf (Complement Si) is Element of bool X
(X,(Complement Si)) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(Complement Si)) is Element of bool X
(lim_inf (Complement Si)) ` is Element of bool X
X \ (lim_inf (Complement Si)) is set
Complement (Complement Si) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup (Complement (Complement Si)) is Element of bool X
(X,(Complement (Complement Si))) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(Complement (Complement Si))) is Element of bool X
(lim_sup (Complement (Complement Si))) ` is Element of bool X
X \ (lim_sup (Complement (Complement Si))) is set
(lim_sup Si) ` is Element of bool X
X \ (lim_sup Si) is set
X is set
bool X is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
the_value_of S is set
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,S) . S is Element of bool X
S is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
(X,S) . S is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,Si) is Element of bool X
Union Si is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,Si) is Element of bool X
Union Si is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,Si) is Element of bool X
Intersection Si is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,Si) is Element of bool X
Intersection Si is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,Si) is Element of bool X
Union Si is Element of bool X
lim_inf Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,Si) is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,Si) is Element of bool X
Intersection Si is Element of bool X
lim_inf Si is Element of bool X
(X,Si) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,Si) is Element of bool X
X is set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty V59() set
bool (bool X) is non empty V59() set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
S is non empty Relation-like NAT -defined Si -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(S) is Relation-like Function-like set
S is V7() V8() V9() V13() V14() ext-real V57() set
S ^\ S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
B is V7() V8() V9() V13() V14() ext-real V57() set
B . B is set
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (B + A3) is Element of bool X
rng S is non empty Element of bool Si
bool Si is non empty V59() set
rng B is non empty Element of bool (bool X)
bool (bool X) is non empty V59() set
Intersection B is Element of bool X
meet (rng B) is Element of bool X
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : A3 <= b1 } is set
meet { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : A3 <= b1 } is set
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
(X,S) . S is set
rng (X,S) is non empty Element of bool (bool X)
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
S is non empty Relation-like NAT -defined Si -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(S) is Relation-like Function-like set
S is V7() V8() V9() V13() V14() ext-real V57() set
S ^\ S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
B is V7() V8() V9() V13() V14() ext-real V57() set
B . B is set
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B + A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (B + A3) is Element of bool X
rng S is non empty Element of bool Si
bool Si is non empty V59() set
rng B is non empty Element of bool (bool X)
bool (bool X) is non empty V59() set
Union B is Element of bool X
union (rng B) is Element of bool X
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
{ (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : A3 <= b1 } is set
union { (S . b1) where b1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT : A3 <= b1 } is set
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
(X,S) . S is set
rng (X,S) is non empty Element of bool (bool X)
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is set
S is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued S -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),B) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),B) is Element of bool X
lim_sup B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,B) is Element of bool X
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is set
S is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued S -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),B) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),B) is Element of bool X
lim_inf B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,B) is Element of bool X
A3 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
Intersection S is Element of bool X
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
0 + B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (0 + B) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
Union S is Element of bool X
S is set
B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
0 + B is V7() V8() V9() V13() V14() ext-real V57() Element of NAT
S . (0 + B) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),S) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),S) is Element of bool X
(X,(bool X),S) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),S) is Element of bool X
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
Complement S is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup (Complement S) is Element of bool X
(X,(Complement S)) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(Complement S)) is Element of bool X
(lim_sup (Complement S)) ` is Element of bool X
X \ (lim_sup (Complement S)) is set
S is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),S) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),S) is Element of bool X
Complement S is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),(Complement S)) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),(Complement S)) is Element of bool X
(Intersection (X,(bool X),(Complement S))) ` is Element of bool X
X \ (Intersection (X,(bool X),(Complement S))) is set
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
lim_sup (Complement S) is Element of bool X
(X,(Complement S)) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(Complement S)) is Element of bool X
(lim_sup (Complement S)) ` is Element of bool X
X \ (lim_sup (Complement S)) is set
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
Complement S is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf (Complement S) is Element of bool X
(X,(Complement S)) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(Complement S)) is Element of bool X
(lim_inf (Complement S)) ` is Element of bool X
X \ (lim_inf (Complement S)) is set
Complement (Complement S) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup (Complement (Complement S)) is Element of bool X
(X,(Complement (Complement S))) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(Complement (Complement S))) is Element of bool X
(lim_sup (Complement (Complement S))) ` is Element of bool X
X \ (lim_sup (Complement (Complement S))) is set
(lim_sup S) ` is Element of bool X
X \ (lim_sup S) is set
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,B) is Element of bool X
(lim_inf S) \/ (lim_inf B) is Element of bool X
A3 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A3) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),A3) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),B) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),B) is Element of bool X
A2 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A2) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),A2) is Element of bool X
(Union (X,(bool X),B)) \/ (Union (X,(bool X),A2)) is Element of bool X
lim_inf B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,B) is Element of bool X
lim_inf A2 is Element of bool X
(X,A2) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,A2) is Element of bool X
lim_inf A3 is Element of bool X
(X,A3) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,A3) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,B) is Element of bool X
(lim_inf S) /\ (lim_inf B) is Element of bool X
A3 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A3) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),A3) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),B) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),B) is Element of bool X
A2 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A2) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),A2) is Element of bool X
(Union (X,(bool X),B)) /\ (Union (X,(bool X),A2)) is Element of bool X
lim_inf B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,B) is Element of bool X
lim_inf A2 is Element of bool X
(X,A2) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,A2) is Element of bool X
lim_inf A3 is Element of bool X
(X,A3) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,A3) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,B) is Element of bool X
(lim_sup S) \/ (lim_sup B) is Element of bool X
A3 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A3) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),A3) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),B) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),B) is Element of bool X
A2 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A2) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),A2) is Element of bool X
(Intersection (X,(bool X),B)) \/ (Intersection (X,(bool X),A2)) is Element of bool X
lim_sup B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,B) is Element of bool X
lim_sup A2 is Element of bool X
(X,A2) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,A2) is Element of bool X
lim_sup A3 is Element of bool X
(X,A3) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,A3) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,B) is Element of bool X
(lim_sup S) /\ (lim_sup B) is Element of bool X
A3 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A3) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),A3) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),B) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),B) is Element of bool X
A2 is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A2) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),A2) is Element of bool X
(Intersection (X,(bool X),B)) /\ (Intersection (X,(bool X),A2)) is Element of bool X
lim_sup B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,B) is Element of bool X
lim_sup A2 is Element of bool X
(X,A2) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,A2) is Element of bool X
lim_sup A3 is Element of bool X
(X,A3) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,A3) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is Element of bool X
S is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued S -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
the_value_of S is set
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
B is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
the_value_of B is set
(X,(bool X),B) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,(bool X),B) is Element of bool X
(X,(bool X),B) is non empty Relation-like NAT -defined bool X -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,(bool X),B) is Element of bool X
lim_inf B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,B) is Element of bool X
lim_sup B is Element of bool X
(X,B) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,B) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
S is non empty Relation-like NAT -defined Si -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
Union S is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
S is non empty Relation-like NAT -defined Si -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
Union S is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
Union S is Element of bool X
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
S is non empty Relation-like NAT -defined Si -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
Intersection S is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
S is non empty Relation-like NAT -defined Si -valued bool X -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
Intersection S is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]
lim_sup S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-ascending Element of bool [:NAT,(bool X):]
Intersection (X,S) is Element of bool X
Intersection S is Element of bool X
lim_inf S is Element of bool X
(X,S) is non empty Relation-like NAT -defined bool X -valued Function-like V28( NAT ) V32( NAT , bool X) non-descending Element of bool [:NAT,(bool X):]
Union (X,S) is Element of bool X
X is set
bool X is non empty V59() set
bool (bool X) is non empty V59() set
bool X is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty V59() set
Si is non empty compl-closed sigma-multiplicative V59() Element of bool (bool X)
S is non empty Relation-like NAT -defined bool X -valued Si -valued Function-like V28( NAT ) V32( NAT , bool X) Element of bool [:NAT,(bool X):]