:: KURATO_0 semantic presentation

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

c

c

F . (c

F ^\ c

(X,(F ^\ c

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

c

(F ^\ m) . c

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

c

y + c

x . (y + c

F . (y + c

n \+\ (F . (y + c

n \ (F . (y + c

(F . (y + c

(n \ (F . (y + c

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

c

y + c

x . (y + c

F . (y + c

n \+\ (F . (y + c

n \ (F . (y + c

(F . (y + c

(n \ (F . (y + c

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