:: SETLIM_1 semantic presentation

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 . b

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 . b

{ (S . b

S . X is Element of Si

{(S . X)} is non empty set

{ (S . b

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 . b

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 . b

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 . b

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 . b

union { (S . b

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 . b

meet { (S . b

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 . b

meet { (Si . b

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 . b

union { (Si . b

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 . b

meet { (X . b

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 . b

Si . B is set

meet { (X . b

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 . b

meet { (Si . b

dom (Si) is set

X is Relation-like Function-like set

{ (X . b

union { (X . b

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 . b

Si . B is set

union { (X . b

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 . b

union { (Si . b

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 . b

meet { (Si . b

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 . b

union { (Si . b

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 . b

meet { (S . b

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 . b

union { (S . b

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 . b

meet { (S . b

S + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT

{ (S . b

S . S is Element of bool Si

{(S . S)} is non empty set

{ (S . b

(Si,S) . (S + 1) is Element of bool Si

meet { (S . b

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 . b

S + 1 is V7() V8() V9() V13() V14() ext-real V57() Element of NAT

{ (S . b

S . S is Element of bool Si

{(S . S)} is non empty set

{ (S . b

union { (S . b

union { (S . b

(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 . b

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 . b

{ ((Complement S) . b

{ ((S . b

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 . b

meet { (S . b

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 . b

union { (S . b

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 . b

union { (S . b

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