REAL is set
NAT is non empty V7() V8() V9() Element of bool REAL
bool REAL is non empty set
NAT is non empty V7() V8() V9() set
bool NAT is non empty set
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
bool NAT is non empty set
RAT is set
INT is set
{} is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding set
the empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding set is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding set
1 is non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative Element of NAT
dom {} is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding set
rng {} is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding set
X is Relation-like Function-like set
dom X is set
meet X is set
F is set
X . F is set
x is set
X is set
F is set
x is set
n is set
[:X,x:] is Relation-like set
[:F,n:] is Relation-like set
m is set
h is set
[m,h] is set
{m,h} is non empty set
{m} is non empty set
{{m,h},{m}} is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
X is non empty set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
the Element of X is Element of X
{ the Element of X} is non empty Element of bool X
x is Element of bool X
NAT --> x is non empty V11() Relation-like NAT -defined bool X -valued Function-like constant V29( NAT ) V33( NAT , bool X) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
m is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
Union F is set
Union F is Element of bool X
meet F is set
rng F is non empty Element of bool (bool X)
bool (bool X) is non empty set
x is Element of bool (bool X)
meet x is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
x is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,x) is Element of bool X
x is Element of bool X
n is Element of bool X
m is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,m) is Element of bool X
h is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,h) is Element of bool X
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
m . y is Element of bool X
h . y is Element of bool X
F ^\ y is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(F ^\ y)) is Element of bool X
x is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,x) is Element of bool X
x is Element of bool X
n is Element of bool X
m is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,m) is Element of bool X
h is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,h) is Element of bool X
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
m . y is Element of bool X
h . y is Element of bool X
F ^\ y is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(F ^\ y)) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
x is set
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
dom F is non empty Element of bool NAT
F . n is Element of bool X
n is set
F . n is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
x is set
n is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,n) is Element of bool X
m is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,m) is Element of bool X
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
m . h is Element of bool X
F ^\ h is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
(F ^\ h) . g is Element of bool X
c8 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
c8 + g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (c8 + g) is Element of bool X
F ^\ c8 is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(F ^\ c8)) is Element of bool X
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F ^\ m is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
(F ^\ m) . y is Element of bool X
m + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (m + y) is Element of bool X
(X,(F ^\ m)) is Element of bool X
n . m is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
x is set
n is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,n) is Element of bool X
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F ^\ m is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
y is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,y) is Element of bool X
y . m is Element of bool X
(X,(F ^\ m)) is Element of bool X
c8 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
(F ^\ m) . c8 is Element of bool X
g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
m + g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (m + g) is Element of bool X
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n . m is Element of bool X
F ^\ m is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
m + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (m + y) is Element of bool X
(X,(F ^\ m)) is Element of bool X
(F ^\ m) . y is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
(X,F) is Element of bool X
x is set
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n + m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (n + m) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
(X,F) is Element of bool X
x is set
0 is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding Element of NAT
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
0 + n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (0 + n) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
(X,F) is Element of bool X
x is set
0 is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding Element of NAT
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
0 + n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (0 + n) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
Complement F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(Complement F)) is Element of bool X
(X,(Complement F)) ` is Element of bool X
X \ (X,(Complement F)) is set
n is set
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
m + h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
(Complement F) . (m + h) is Element of bool X
F . (m + h) is Element of bool X
(F . (m + h)) ` is Element of bool X
X \ (F . (m + h)) is set
n is set
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
m + h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (m + h) is Element of bool X
(F . (m + h)) ` is Element of bool X
X \ (F . (m + h)) is set
(Complement F) . (m + h) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
n is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
x is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,n) is Element of bool X
(X,F) is Element of bool X
(X,x) is Element of bool X
(X,F) /\ (X,x) is Element of bool X
m is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
x . (h + y) is Element of bool X
n . (h + y) is Element of bool X
F . (h + y) is Element of bool X
(F . (h + y)) /\ (x . (h + y)) is Element of bool X
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (h + y) is Element of bool X
n . (h + y) is Element of bool X
x . (h + y) is Element of bool X
(F . (h + y)) /\ (x . (h + y)) is Element of bool X
m is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
max (h,y) is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
(max (h,y)) + g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
x . ((max (h,y)) + g) is Element of bool X
h is V7() V8() V9() V13() V14() V15() ext-real non negative set
y + h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
g + g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y + (g + g) is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
x . (y + (g + g)) is Element of bool X
g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
(max (h,y)) + g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . ((max (h,y)) + g) is Element of bool X
h is V7() V8() V9() V13() V14() V15() ext-real non negative set
h + h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
g + g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + (g + g) is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (h + (g + g)) is Element of bool X
g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
(max (h,y)) + g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n . ((max (h,y)) + g) is Element of bool X
F . ((max (h,y)) + g) is Element of bool X
x . ((max (h,y)) + g) is Element of bool X
(F . ((max (h,y)) + g)) /\ (x . ((max (h,y)) + g)) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
n is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
x is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,n) is Element of bool X
(X,F) is Element of bool X
(X,x) is Element of bool X
(X,F) \/ (X,x) is Element of bool X
m is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
max (h,y) is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
g is V7() V8() V9() V13() V14() V15() ext-real non negative set
h + g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h is V7() V8() V9() V13() V14() V15() ext-real non negative set
y + h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
k is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
(max (h,y)) + k is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n . ((max (h,y)) + k) is Element of bool X
F . ((max (h,y)) + k) is Element of bool X
x . ((max (h,y)) + k) is Element of bool X
(F . ((max (h,y)) + k)) \/ (x . ((max (h,y)) + k)) is Element of bool X
g is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
g + k is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + (g + k) is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (h + (g + k)) is Element of bool X
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + k is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y + (h + k) is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
x . (y + (h + k)) is Element of bool X
m is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (h + y) is Element of bool X
n . (h + y) is Element of bool X
x . (h + y) is Element of bool X
(F . (h + y)) \/ (x . (h + y)) is Element of bool X
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
x . (h + y) is Element of bool X
n . (h + y) is Element of bool X
F . (h + y) is Element of bool X
(F . (h + y)) \/ (x . (h + y)) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
n is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
x is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
(X,x) is Element of bool X
(X,F) \/ (X,x) is Element of bool X
(X,n) is Element of bool X
m is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n . (h + y) is Element of bool X
F . (h + y) is Element of bool X
x . (h + y) is Element of bool X
(F . (h + y)) \/ (x . (h + y)) is Element of bool X
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n . (h + y) is Element of bool X
x . (h + y) is Element of bool X
F . (h + y) is Element of bool X
(F . (h + y)) \/ (x . (h + y)) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
n is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
x is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,n) is Element of bool X
(X,F) is Element of bool X
(X,x) is Element of bool X
(X,F) /\ (X,x) is Element of bool X
m is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n . (h + y) is Element of bool X
x . (h + y) is Element of bool X
F . (h + y) is Element of bool X
(F . (h + y)) /\ (x . (h + y)) is Element of bool X
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n . (h + y) is Element of bool X
F . (h + y) is Element of bool X
x . (h + y) is Element of bool X
(F . (h + y)) /\ (x . (h + y)) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
x is Element of bool X
n is set
0 is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding Element of NAT
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
0 + m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (0 + m) is Element of bool X
n is set
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
0 is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding Element of NAT
m + 0 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (m + 0) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
x is Element of bool X
n is set
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
0 is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding Element of NAT
m + 0 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (m + 0) is Element of bool X
n is set
0 is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding Element of NAT
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
0 + m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (0 + m) is Element of bool X
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
x is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
(X,x) is Element of bool X
n is Element of bool X
n \+\ (X,F) is Element of bool X
n \ (X,F) is set
(X,F) \ n is set
(n \ (X,F)) \/ ((X,F) \ n) is set
m is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (h + y) is Element of bool X
x . (h + y) is Element of bool X
n \+\ (F . (h + y)) is Element of bool X
n \ (F . (h + y)) is set
(F . (h + y)) \ n is set
(n \ (F . (h + y))) \/ ((F . (h + y)) \ n) is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
c8 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y + c8 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
x . (y + c8) is Element of bool X
F . (y + c8) is Element of bool X
n \+\ (F . (y + c8)) is Element of bool X
n \ (F . (y + c8)) is set
(F . (y + c8)) \ n is set
(n \ (F . (y + c8))) \/ ((F . (y + c8)) \ n) is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
x is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
(X,x) is Element of bool X
n is Element of bool X
n \+\ (X,F) is Element of bool X
n \ (X,F) is set
(X,F) \ n is set
(n \ (X,F)) \/ ((X,F) \ n) is set
m is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
c8 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y + c8 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
x . (y + c8) is Element of bool X
F . (y + c8) is Element of bool X
n \+\ (F . (y + c8)) is Element of bool X
n \ (F . (y + c8)) is set
(F . (y + c8)) \ n is set
(n \ (F . (y + c8))) \/ ((F . (y + c8)) \ n) is set
h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
h + y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (h + y) is Element of bool X
x . (h + y) is Element of bool X
n \+\ (F . (h + y)) is Element of bool X
n \ (F . (h + y)) is set
(F . (h + y)) \ n is set
(n \ (F . (h + y))) \/ ((F . (h + y)) \ n) is set
X is Relation-like Function-like set
F is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
x is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
X . x is set
X . F is set
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F + n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
X . (F + n) is set
(F + n) + 1 is non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative Element of NAT
n + 1 is non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative Element of NAT
F + (n + 1) is non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative Element of NAT
X . (F + (n + 1)) is set
0 is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding Element of NAT
F + 0 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
X . (F + 0) is set
n is V7() V8() V9() V13() V14() V15() ext-real non negative set
F + n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
x is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
x + 1 is non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative Element of NAT
F . (x + 1) is Element of bool X
F . x is Element of bool X
x is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . n is Element of bool X
F . x is Element of bool X
x is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . x is Element of bool X
x + 1 is non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative Element of NAT
F . (x + 1) is Element of bool X
x is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . x is Element of bool X
F . n is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
x is set
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
n + 1 is non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative Element of NAT
F . (n + 1) is Element of bool X
rng F is non empty Element of bool (bool X)
bool (bool X) is non empty set
meet (rng F) is Element of bool X
m is set
dom F is non empty Element of bool NAT
h is set
F . h is set
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . n is Element of bool X
F . y is Element of bool X
y is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
(X,F) is Element of bool X
x is set
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . m is Element of bool X
h is V7() V8() V9() V13() V14() V15() ext-real non negative set
n + h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
(X,F) is Element of bool X
x is set
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . n is Element of bool X
m is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
0 is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding Element of NAT
m + 0 is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . (m + 0) is Element of bool X
F . m is Element of bool X
h is V7() V8() V9() V13() V14() V15() ext-real non negative set
m + h is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
the_value_of F is set
dom F is non empty Element of bool NAT
x is set
F . x is set
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . n is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
x is Element of bool X
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . n is Element of bool X
n + 1 is non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative Element of NAT
F . (n + 1) is Element of bool X
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT
F . n is Element of bool X
n + 1 is non empty V7() V8() V9() V13() V14() V15() ext-real positive non negative Element of NAT
F . (n + 1) is Element of bool X
(X,F) is Element of bool X
(X,F) is Element of bool X
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
{} X is empty V7() V8() V9() V11() V12() V13() V14() V15() ext-real non positive non negative Relation-like non-empty empty-yielding Element of bool X
NAT --> ({} X) is non empty V11() Relation-like NAT -defined bool X -valued Function-like constant V29( NAT ) V33( NAT , bool X) V33( NAT , bool X) non-ascending non-descending (X) Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) Element of bool [:NAT,(bool X):]
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:NAT,(bool X):] is non empty Relation-like set
bool [:NAT,(bool X):] is non empty set
F is non empty Relation-like NAT -defined bool X -valued Function-like V29( NAT ) V33( NAT , bool X) (X) Element of bool [:NAT,(bool X):]
(X,F) is Element of bool X
x is set
(X,F) is Element of bool X
n is V7() V8() V9() V13() V14() V15() ext-real non negative Element of NAT