:: YELLOW15 semantic presentation

REAL is set

NAT is V9() V10() V11() V12() non empty non trivial non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

NAT is V9() V10() V11() V12() non empty non trivial non finite cardinal limit_cardinal set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

BOOLEAN is non empty set

0 is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of NAT

{} is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set

the Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set

1 is V2() V9() V10() V11() V15() non empty finite cardinal Element of NAT

{0,1} is non empty finite V31() set

2 is V2() V9() V10() V11() V15() non empty finite cardinal Element of NAT

3 is V2() V9() V10() V11() V15() non empty finite cardinal Element of NAT

dom {} is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set

rng {} is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain with_non-empty_elements set

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

K182() is set

K183() is set

F

Seg F

F

T is set

F

F

[:(Seg F

bool [:(Seg F

T is Relation-like Seg F

dom T is finite Element of bool (Seg F

bool (Seg F

tT is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng tT is finite set

B is Relation-like NAT -defined F

len B is V9() V10() V11() V15() finite cardinal Element of NAT

x is V9() V10() V11() V15() finite cardinal set

B . x is set

F

F

T is set

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

tT is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len tT is V9() V10() V11() V15() finite cardinal Element of NAT

dom tT is finite Element of bool NAT

B is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

TRUE is boolean Element of BOOLEAN

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len x is V9() V10() V11() V15() finite cardinal Element of NAT

dom x is finite Element of bool NAT

rng x is finite set

sfA is set

sfA is V9() V10() V11() V15() finite cardinal set

x . sfA is set

B . sfA is set

tT . sfA is set

T \ (tT . sfA) is Element of bool T

IFEQ ((B . sfA),TRUE,(tT . sfA),(T \ (tT . sfA))) is set

Seg (len tT) is finite len tT -element Element of bool NAT

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

dom sfA is finite Element of bool NAT

sfA is V9() V10() V11() V15() finite cardinal set

sfA . sfA is set

B . sfA is set

tT . sfA is set

T \ (tT . sfA) is Element of bool T

IFEQ ((B . sfA),TRUE,(tT . sfA),(T \ (tT . sfA))) is set

x is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len x is V9() V10() V11() V15() finite cardinal Element of NAT

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

dom x is finite Element of bool NAT

Seg (len tT) is finite len tT -element Element of bool NAT

sfA is V9() V10() V11() V15() finite cardinal set

x . sfA is set

B . sfA is set

tT . sfA is set

T \ (tT . sfA) is Element of bool T

IFEQ ((B . sfA),TRUE,(tT . sfA),(T \ (tT . sfA))) is set

sfA . sfA is set

T is set

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

tT is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

dom tT is finite Element of bool NAT

B is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

(T,tT,B) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

dom (T,tT,B) is finite Element of bool NAT

len (T,tT,B) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,tT,B)) is finite len (T,tT,B) -element Element of bool NAT

len tT is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len tT) is finite len tT -element Element of bool NAT

T is set

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

tT is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

B is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

(T,tT,B) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

x is V9() V10() V11() V15() finite cardinal set

B . x is set

(T,tT,B) . x is set

tT . x is set

dom tT is finite Element of bool NAT

T \ (tT . x) is Element of bool T

IFEQ ((B . x),TRUE,(tT . x),(T \ (tT . x))) is set

dom tT is finite Element of bool NAT

len tT is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len tT) is finite len tT -element Element of bool NAT

len (T,tT,B) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,tT,B)) is finite len (T,tT,B) -element Element of bool NAT

dom (T,tT,B) is finite Element of bool NAT

dom tT is finite Element of bool NAT

FALSE is boolean Element of BOOLEAN

T is set

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

tT is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

dom tT is finite Element of bool NAT

B is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

(T,tT,B) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

x is V9() V10() V11() V15() finite cardinal set

B . x is set

(T,tT,B) . x is set

tT . x is set

T \ (tT . x) is Element of bool T

IFEQ ((B . x),TRUE,(tT . x),(T \ (tT . x))) is set

T is set

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

<*> (bool T) is Relation-like non-empty empty-yielding NAT -defined bool T -valued V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial proper finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of bool T

[:NAT,(bool T):] is Relation-like non empty non trivial non finite set

tT is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

(T,(<*> (bool T)),tT) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len (T,(<*> (bool T)),tT) is V9() V10() V11() V15() finite cardinal Element of NAT

len (<*> (bool T)) is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of NAT

T is set

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

<*> (bool T) is Relation-like non-empty empty-yielding NAT -defined bool T -valued V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial proper finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of bool T

[:NAT,(bool T):] is Relation-like non empty non trivial non finite set

tT is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

(T,(<*> (bool T)),tT) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len (T,(<*> (bool T)),tT) is V9() V10() V11() V15() finite cardinal Element of NAT

len (<*> (bool T)) is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of NAT

T is set

bool T is non empty set

tT is Element of bool T

<*tT*> is Relation-like NAT -defined bool T -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of bool T

B is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

(T,<*tT*>,B) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

bool T is non empty Element of bool (bool T)

bool (bool T) is non empty set

len (T,<*tT*>,B) is V9() V10() V11() V15() finite cardinal Element of NAT

len <*tT*> is V9() V10() V11() V15() non empty finite cardinal Element of NAT

T is set

bool T is non empty set

tT is Element of bool T

<*tT*> is Relation-like NAT -defined bool T -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of bool T

T \ tT is Element of bool T

B is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

B . 1 is set

(T,<*tT*>,B) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

bool T is non empty Element of bool (bool T)

bool (bool T) is non empty set

(T,<*tT*>,B) . 1 is set

<*tT*> . 1 is set

dom <*tT*> is non empty trivial finite 1 -element Element of bool NAT

<*tT*> . 1 is set

T \ (<*tT*> . 1) is Element of bool T

T is set

bool T is non empty set

tT is Element of bool T

B is Element of bool T

<*tT,B*> is Relation-like NAT -defined bool T -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of bool T

x is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

(T,<*tT,B*>,x) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

bool T is non empty Element of bool (bool T)

bool (bool T) is non empty set

len (T,<*tT,B*>,x) is V9() V10() V11() V15() finite cardinal Element of NAT

len <*tT,B*> is V9() V10() V11() V15() non empty finite cardinal Element of NAT

T is set

bool T is non empty set

tT is Element of bool T

B is Element of bool T

<*tT,B*> is Relation-like NAT -defined bool T -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of bool T

T \ tT is Element of bool T

T \ B is Element of bool T

x is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

x . 1 is set

(T,<*tT,B*>,x) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

bool T is non empty Element of bool (bool T)

bool (bool T) is non empty set

(T,<*tT,B*>,x) . 1 is set

x . 2 is set

(T,<*tT,B*>,x) . 2 is set

<*tT,B*> . 1 is set

Seg 2 is non empty finite 2 -element Element of bool NAT

dom <*tT,B*> is non empty finite 2 -element Element of bool NAT

<*tT,B*> . 1 is set

T \ (<*tT,B*> . 1) is Element of bool T

<*tT,B*> . 2 is set

<*tT,B*> . 2 is set

T \ (<*tT,B*> . 2) is Element of bool T

T is set

bool T is non empty set

tT is Element of bool T

B is Element of bool T

x is Element of bool T

<*tT,B,x*> is Relation-like NAT -defined bool T -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of bool T

sfA is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

(T,<*tT,B,x*>,sfA) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

bool T is non empty Element of bool (bool T)

bool (bool T) is non empty set

len (T,<*tT,B,x*>,sfA) is V9() V10() V11() V15() finite cardinal Element of NAT

len <*tT,B,x*> is V9() V10() V11() V15() non empty finite cardinal Element of NAT

T is set

bool T is non empty set

tT is Element of bool T

B is Element of bool T

x is Element of bool T

<*tT,B,x*> is Relation-like NAT -defined bool T -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of bool T

T \ tT is Element of bool T

T \ B is Element of bool T

T \ x is Element of bool T

sfA is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

sfA . 1 is set

(T,<*tT,B,x*>,sfA) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

bool T is non empty Element of bool (bool T)

bool (bool T) is non empty set

(T,<*tT,B,x*>,sfA) . 1 is set

sfA . 2 is set

(T,<*tT,B,x*>,sfA) . 2 is set

sfA . 3 is set

(T,<*tT,B,x*>,sfA) . 3 is set

<*tT,B,x*> . 1 is set

Seg 3 is non empty finite 3 -element Element of bool NAT

dom <*tT,B,x*> is non empty finite 3 -element Element of bool NAT

<*tT,B,x*> . 1 is set

T \ (<*tT,B,x*> . 1) is Element of bool T

<*tT,B,x*> . 2 is set

<*tT,B,x*> . 2 is set

T \ (<*tT,B,x*> . 2) is Element of bool T

<*tT,B,x*> . 3 is set

<*tT,B,x*> . 3 is set

T \ (<*tT,B,x*> . 3) is Element of bool T

T is set

bool T is non empty Element of bool (bool T)

bool T is non empty set

bool (bool T) is non empty set

tT is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len tT is V9() V10() V11() V15() finite cardinal Element of NAT

{ (Intersect (rng (T,tT,b

B is set

x is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

(T,tT,x) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,tT,x) is finite Element of bool (bool T)

bool (bool T) is non empty set

Intersect (rng (T,tT,x)) is Element of bool T

len x is V9() V10() V11() V15() finite cardinal Element of NAT

T is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN

rng T is finite Element of bool BOOLEAN

bool BOOLEAN is non empty set

T is set

bool T is non empty set

bool (bool T) is non empty set

bool T is non empty Element of bool (bool T)

tT is finite Element of bool (bool T)

card tT is V9() V10() V11() V15() finite cardinal Element of NAT

B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng B is finite set

x is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len x is V9() V10() V11() V15() finite cardinal Element of NAT

{ (Intersect (rng (T,x,b

sfA is Element of bool (bool T)

rng x is finite Element of bool (bool T)

bool (bool T) is non empty set

B is Element of bool (bool T)

x is Element of bool (bool T)

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

rng sfA is finite Element of bool (bool T)

bool (bool T) is non empty set

{ (Intersect (rng (T,sfA,b

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

rng sfA is finite Element of bool (bool T)

bool (bool T) is non empty set

{ (Intersect (rng (T,sfA,b

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

rng sfA is finite Element of bool (bool T)

{ (Intersect (rng (T,sfA,b

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

rng sfA is finite Element of bool (bool T)

{ (Intersect (rng (T,sfA,b

a is Element of bool T

dom sfA is finite Element of bool NAT

[:(dom sfA),(rng sfA):] is Relation-like finite set

bool [:(dom sfA),(rng sfA):] is non empty finite V31() set

sfA " is Relation-like Function-like set

[:(rng sfA),(dom sfA):] is Relation-like finite set

bool [:(rng sfA),(dom sfA):] is non empty finite V31() set

sfA * (sfA ") is Relation-like NAT -defined Function-like finite set

z is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

(T,sfA,z) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,sfA,z) is finite Element of bool (bool T)

Intersect (rng (T,sfA,z)) is Element of bool T

len z is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len z) is finite len z -element Element of bool NAT

dom z is finite Element of bool NAT

[:(dom sfA),BOOLEAN:] is Relation-like set

bool [:(dom sfA),BOOLEAN:] is non empty set

(sfA * (sfA ")) * z is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(sfA ") * z is Relation-like BOOLEAN -valued Function-like set

sfA * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

dom (sfA ") is set

dom (sfA * (sfA ")) is finite Element of bool NAT

dom sfA is finite Element of bool NAT

rng (sfA * (sfA ")) is finite set

rng (sfA ") is set

dom ((sfA * (sfA ")) * z) is finite Element of bool NAT

sfA " is Relation-like Function-like set

dom (sfA ") is set

sfA * (sfA ") is Relation-like NAT -defined Function-like finite set

dom (sfA * (sfA ")) is finite Element of bool NAT

y1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

len y1 is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len y1) is finite len y1 -element Element of bool NAT

dom y1 is finite Element of bool NAT

Seg (len sfA) is finite len sfA -element Element of bool NAT

rng (sfA * (sfA ")) is finite set

rng (sfA ") is set

(sfA * (sfA ")) * y1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

dom ((sfA * (sfA ")) * y1) is finite Element of bool NAT

(sfA ") * y1 is Relation-like BOOLEAN -valued Function-like set

sfA * ((sfA ") * y1) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(sfA * (sfA ")) * (sfA * ((sfA ") * z)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(sfA * (sfA ")) * sfA is Relation-like NAT -defined bool T -valued Function-like finite set

((sfA * (sfA ")) * sfA) * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(sfA ") * sfA is Relation-like bool T -valued Function-like set

sfA * ((sfA ") * sfA) is Relation-like NAT -defined bool T -valued Function-like finite set

(sfA * ((sfA ") * sfA)) * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

id (rng sfA) is Relation-like rng sfA -defined rng sfA -valued Function-like one-to-one set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

sfA * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

sfA * (sfA ") is Relation-like NAT -defined Function-like finite set

(sfA * (sfA ")) * z is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

id (dom sfA) is Relation-like dom sfA -defined dom sfA -valued Function-like one-to-one set

(id (dom sfA)) * z is Relation-like dom sfA -defined BOOLEAN -valued Function-like set

(T,sfA,y1) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,sfA,y1) is finite Element of bool (bool T)

Y is set

dom (T,sfA,z) is finite Element of bool NAT

i is V9() V10() V11() V15() finite cardinal set

(T,sfA,z) . i is set

len (T,sfA,z) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,sfA,z)) is finite len (T,sfA,z) -element Element of bool NAT

Seg (len sfA) is finite len sfA -element Element of bool NAT

(sfA * (sfA ")) . i is set

z . i is boolean set

((sfA * (sfA ")) * y1) . i is set

y1 . ((sfA * (sfA ")) . i) is boolean set

(T,sfA,y1) . ((sfA * (sfA ")) . i) is set

i is V9() V10() V11() V15() finite cardinal Element of NAT

sfA . i is set

((sfA * (sfA ")) * sfA) . i is set

(sfA * ((sfA ") * sfA)) . i is set

id (rng sfA) is Relation-like rng sfA -defined rng sfA -valued Function-like one-to-one set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

sfA . i is set

(T,sfA,y1) . ((sfA * (sfA ")) . i) is set

i is V9() V10() V11() V15() finite cardinal Element of NAT

sfA . i is set

T \ (sfA . i) is Element of bool T

((sfA * (sfA ")) * sfA) . i is set

T \ (((sfA * (sfA ")) * sfA) . i) is Element of bool T

(sfA * ((sfA ") * sfA)) . i is set

T \ ((sfA * ((sfA ") * sfA)) . i) is Element of bool T

id (rng sfA) is Relation-like rng sfA -defined rng sfA -valued Function-like one-to-one set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

T \ ((sfA * (id (rng sfA))) . i) is Element of bool T

sfA . i is set

T \ (sfA . i) is Element of bool T

(T,sfA,y1) . ((sfA * (sfA ")) . i) is set

(T,sfA,y1) . ((sfA * (sfA ")) . i) is set

len (T,sfA,y1) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,sfA,y1)) is finite len (T,sfA,y1) -element Element of bool NAT

dom (T,sfA,y1) is finite Element of bool NAT

Y is set

dom (T,sfA,y1) is finite Element of bool NAT

i is V9() V10() V11() V15() finite cardinal set

(T,sfA,y1) . i is set

len (T,sfA,y1) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,sfA,y1)) is finite len (T,sfA,y1) -element Element of bool NAT

(sfA * (sfA ")) . i is set

y1 . i is boolean set

((sfA * (sfA ")) * z) . i is set

z . ((sfA * (sfA ")) . i) is boolean set

(T,sfA,z) . ((sfA * (sfA ")) . i) is set

i is V9() V10() V11() V15() finite cardinal Element of NAT

sfA . i is set

(sfA * (sfA ")) * sfA is Relation-like NAT -defined bool T -valued Function-like finite set

((sfA * (sfA ")) * sfA) . i is set

(sfA ") * sfA is Relation-like bool T -valued Function-like set

sfA * ((sfA ") * sfA) is Relation-like NAT -defined bool T -valued Function-like finite set

(sfA * ((sfA ") * sfA)) . i is set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

sfA . i is set

(T,sfA,z) . ((sfA * (sfA ")) . i) is set

i is V9() V10() V11() V15() finite cardinal Element of NAT

sfA . i is set

T \ (sfA . i) is Element of bool T

(sfA * (sfA ")) * sfA is Relation-like NAT -defined bool T -valued Function-like finite set

((sfA * (sfA ")) * sfA) . i is set

T \ (((sfA * (sfA ")) * sfA) . i) is Element of bool T

(sfA ") * sfA is Relation-like bool T -valued Function-like set

sfA * ((sfA ") * sfA) is Relation-like NAT -defined bool T -valued Function-like finite set

(sfA * ((sfA ") * sfA)) . i is set

T \ ((sfA * ((sfA ") * sfA)) . i) is Element of bool T

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

T \ ((sfA * (id (rng sfA))) . i) is Element of bool T

sfA . i is set

T \ (sfA . i) is Element of bool T

(T,sfA,z) . ((sfA * (sfA ")) . i) is set

(T,sfA,z) . ((sfA * (sfA ")) . i) is set

Seg (len sfA) is finite len sfA -element Element of bool NAT

len (T,sfA,z) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,sfA,z)) is finite len (T,sfA,z) -element Element of bool NAT

dom (T,sfA,z) is finite Element of bool NAT

Intersect (rng (T,sfA,y1)) is Element of bool T

dom sfA is finite Element of bool NAT

[:(dom sfA),(rng sfA):] is Relation-like finite set

bool [:(dom sfA),(rng sfA):] is non empty finite V31() set

sfA " is Relation-like Function-like set

[:(rng sfA),(dom sfA):] is Relation-like finite set

bool [:(rng sfA),(dom sfA):] is non empty finite V31() set

sfA * (sfA ") is Relation-like NAT -defined Function-like finite set

z is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

(T,sfA,z) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,sfA,z) is finite Element of bool (bool T)

Intersect (rng (T,sfA,z)) is Element of bool T

len z is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len z) is finite len z -element Element of bool NAT

dom z is finite Element of bool NAT

[:(dom sfA),BOOLEAN:] is Relation-like set

bool [:(dom sfA),BOOLEAN:] is non empty set

(sfA * (sfA ")) * z is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(sfA ") * z is Relation-like BOOLEAN -valued Function-like set

sfA * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

dom (sfA ") is set

dom (sfA * (sfA ")) is finite Element of bool NAT

dom sfA is finite Element of bool NAT

rng (sfA * (sfA ")) is finite set

rng (sfA ") is set

dom ((sfA * (sfA ")) * z) is finite Element of bool NAT

sfA " is Relation-like Function-like set

dom (sfA ") is set

sfA * (sfA ") is Relation-like NAT -defined Function-like finite set

dom (sfA * (sfA ")) is finite Element of bool NAT

y1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

len y1 is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len y1) is finite len y1 -element Element of bool NAT

dom y1 is finite Element of bool NAT

Seg (len sfA) is finite len sfA -element Element of bool NAT

rng (sfA * (sfA ")) is finite set

rng (sfA ") is set

(sfA * (sfA ")) * y1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

dom ((sfA * (sfA ")) * y1) is finite Element of bool NAT

(sfA ") * y1 is Relation-like BOOLEAN -valued Function-like set

sfA * ((sfA ") * y1) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(sfA * (sfA ")) * (sfA * ((sfA ") * z)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(sfA * (sfA ")) * sfA is Relation-like NAT -defined bool T -valued Function-like finite set

((sfA * (sfA ")) * sfA) * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(sfA ") * sfA is Relation-like bool T -valued Function-like set

sfA * ((sfA ") * sfA) is Relation-like NAT -defined bool T -valued Function-like finite set

(sfA * ((sfA ") * sfA)) * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

id (rng sfA) is Relation-like rng sfA -defined rng sfA -valued Function-like one-to-one set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

sfA * ((sfA ") * z) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

sfA * (sfA ") is Relation-like NAT -defined Function-like finite set

(sfA * (sfA ")) * z is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

id (dom sfA) is Relation-like dom sfA -defined dom sfA -valued Function-like one-to-one set

(id (dom sfA)) * z is Relation-like dom sfA -defined BOOLEAN -valued Function-like set

(T,sfA,y1) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,sfA,y1) is finite Element of bool (bool T)

Y is set

dom (T,sfA,z) is finite Element of bool NAT

i is V9() V10() V11() V15() finite cardinal set

(T,sfA,z) . i is set

len (T,sfA,z) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,sfA,z)) is finite len (T,sfA,z) -element Element of bool NAT

Seg (len sfA) is finite len sfA -element Element of bool NAT

(sfA * (sfA ")) . i is set

z . i is boolean set

((sfA * (sfA ")) * y1) . i is set

y1 . ((sfA * (sfA ")) . i) is boolean set

(T,sfA,y1) . ((sfA * (sfA ")) . i) is set

i is V9() V10() V11() V15() finite cardinal Element of NAT

sfA . i is set

((sfA * (sfA ")) * sfA) . i is set

(sfA * ((sfA ") * sfA)) . i is set

id (rng sfA) is Relation-like rng sfA -defined rng sfA -valued Function-like one-to-one set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

sfA . i is set

(T,sfA,y1) . ((sfA * (sfA ")) . i) is set

i is V9() V10() V11() V15() finite cardinal Element of NAT

sfA . i is set

T \ (sfA . i) is Element of bool T

((sfA * (sfA ")) * sfA) . i is set

T \ (((sfA * (sfA ")) * sfA) . i) is Element of bool T

(sfA * ((sfA ") * sfA)) . i is set

T \ ((sfA * ((sfA ") * sfA)) . i) is Element of bool T

id (rng sfA) is Relation-like rng sfA -defined rng sfA -valued Function-like one-to-one set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

T \ ((sfA * (id (rng sfA))) . i) is Element of bool T

sfA . i is set

T \ (sfA . i) is Element of bool T

(T,sfA,y1) . ((sfA * (sfA ")) . i) is set

(T,sfA,y1) . ((sfA * (sfA ")) . i) is set

len (T,sfA,y1) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,sfA,y1)) is finite len (T,sfA,y1) -element Element of bool NAT

dom (T,sfA,y1) is finite Element of bool NAT

Y is set

dom (T,sfA,y1) is finite Element of bool NAT

i is V9() V10() V11() V15() finite cardinal set

(T,sfA,y1) . i is set

len (T,sfA,y1) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,sfA,y1)) is finite len (T,sfA,y1) -element Element of bool NAT

(sfA * (sfA ")) . i is set

y1 . i is boolean set

((sfA * (sfA ")) * z) . i is set

z . ((sfA * (sfA ")) . i) is boolean set

(T,sfA,z) . ((sfA * (sfA ")) . i) is set

i is V9() V10() V11() V15() finite cardinal Element of NAT

sfA . i is set

(sfA * (sfA ")) * sfA is Relation-like NAT -defined bool T -valued Function-like finite set

((sfA * (sfA ")) * sfA) . i is set

(sfA ") * sfA is Relation-like bool T -valued Function-like set

sfA * ((sfA ") * sfA) is Relation-like NAT -defined bool T -valued Function-like finite set

(sfA * ((sfA ") * sfA)) . i is set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

sfA . i is set

(T,sfA,z) . ((sfA * (sfA ")) . i) is set

i is V9() V10() V11() V15() finite cardinal Element of NAT

sfA . i is set

T \ (sfA . i) is Element of bool T

(sfA * (sfA ")) * sfA is Relation-like NAT -defined bool T -valued Function-like finite set

((sfA * (sfA ")) * sfA) . i is set

T \ (((sfA * (sfA ")) * sfA) . i) is Element of bool T

(sfA ") * sfA is Relation-like bool T -valued Function-like set

sfA * ((sfA ") * sfA) is Relation-like NAT -defined bool T -valued Function-like finite set

(sfA * ((sfA ") * sfA)) . i is set

T \ ((sfA * ((sfA ") * sfA)) . i) is Element of bool T

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

T \ ((sfA * (id (rng sfA))) . i) is Element of bool T

sfA . i is set

T \ (sfA . i) is Element of bool T

(T,sfA,z) . ((sfA * (sfA ")) . i) is set

(T,sfA,z) . ((sfA * (sfA ")) . i) is set

Seg (len sfA) is finite len sfA -element Element of bool NAT

len (T,sfA,z) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,sfA,z)) is finite len (T,sfA,z) -element Element of bool NAT

dom (T,sfA,z) is finite Element of bool NAT

Intersect (rng (T,sfA,y1)) is Element of bool T

T is set

bool T is non empty set

bool (bool T) is non empty set

tT is finite Element of bool (bool T)

(T,tT) is Element of bool (bool T)

bool T is non empty Element of bool (bool T)

card tT is V9() V10() V11() V15() finite cardinal Element of NAT

B is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len B is V9() V10() V11() V15() finite cardinal Element of NAT

rng B is finite Element of bool (bool T)

bool (bool T) is non empty set

{ (Intersect (rng (T,B,b

BOOLEAN * is functional non empty FinSequence-membered FinSequenceSet of BOOLEAN

(len B) -tuples_on BOOLEAN is functional non empty FinSequence-membered with_common_domain product-like FinSequenceSet of BOOLEAN

{ b

{ (Intersect (rng (T,B,b

x is set

sfA is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

(T,B,sfA) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,B,sfA) is finite Element of bool (bool T)

Intersect (rng (T,B,sfA)) is Element of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

(len sfA) -tuples_on BOOLEAN is functional non empty FinSequence-membered with_common_domain product-like FinSequenceSet of BOOLEAN

{ b

{ H

T is set

bool T is non empty set

bool (bool T) is non empty set

{T} is non empty trivial finite 1 -element set

tT is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial proper finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of bool (bool T)

(T,tT) is finite Element of bool (bool T)

bool T is non empty Element of bool (bool T)

card tT is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of NAT

B is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len B is V9() V10() V11() V15() finite cardinal Element of NAT

rng B is finite Element of bool (bool T)

bool (bool T) is non empty set

{ (Intersect (rng (T,B,b

x is set

sfA is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

(T,B,sfA) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,B,sfA) is finite Element of bool (bool T)

Intersect (rng (T,B,sfA)) is Element of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

<*> (bool T) is Relation-like non-empty empty-yielding NAT -defined bool T -valued V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial proper finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of bool T

[:NAT,(bool T):] is Relation-like non empty non trivial non finite set

x is set

<*> (bool T) is Relation-like non-empty empty-yielding NAT -defined bool T -valued V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial proper finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of bool T

[:NAT,(bool T):] is Relation-like non empty non trivial non finite set

<*> BOOLEAN is Relation-like non-empty empty-yielding NAT -defined BOOLEAN -valued V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial proper finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain boolean-valued FinSequence of BOOLEAN

[:NAT,BOOLEAN:] is Relation-like non empty non trivial non finite set

(T,B,(<*> BOOLEAN)) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,B,(<*> BOOLEAN)) is finite Element of bool (bool T)

Intersect (rng (T,B,(<*> BOOLEAN))) is Element of bool T

T is set

bool T is non empty set

bool (bool T) is non empty set

B is finite Element of bool (bool T)

tT is finite Element of bool (bool T)

(T,tT) is finite Element of bool (bool T)

(T,B) is finite Element of bool (bool T)

bool T is non empty Element of bool (bool T)

card tT is V9() V10() V11() V15() finite cardinal Element of NAT

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

rng sfA is finite Element of bool (bool T)

bool (bool T) is non empty set

{ (Intersect (rng (T,sfA,b

card B is V9() V10() V11() V15() finite cardinal Element of NAT

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

rng sfA is finite Element of bool (bool T)

{ (Intersect (rng (T,sfA,b

x is set

a is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

(T,sfA,a) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,sfA,a) is finite Element of bool (bool T)

Intersect (rng (T,sfA,a)) is Element of bool T

len a is V9() V10() V11() V15() finite cardinal Element of NAT

dom sfA is finite Element of bool NAT

dom a is finite Element of bool NAT

[:(dom sfA),BOOLEAN:] is Relation-like set

bool [:(dom sfA),BOOLEAN:] is non empty set

sfA " is Relation-like Function-like set

dom (sfA ") is set

rng (sfA ") is set

sfA * (sfA ") is Relation-like NAT -defined Function-like finite set

rng (sfA * (sfA ")) is finite set

[:(dom sfA),(rng sfA):] is Relation-like finite set

bool [:(dom sfA),(rng sfA):] is non empty finite V31() set

[:(rng sfA),(dom sfA):] is Relation-like finite set

bool [:(rng sfA),(dom sfA):] is non empty finite V31() set

(sfA * (sfA ")) * a is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(sfA ") * a is Relation-like BOOLEAN -valued Function-like set

sfA * ((sfA ") * a) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

z is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

(T,sfA,z) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,sfA,z) is finite Element of bool (bool T)

Intersect (rng (T,sfA,z)) is Element of bool T

y1 is set

dom z is finite Element of bool NAT

dom ((sfA * (sfA ")) * a) is finite Element of bool NAT

dom (sfA * (sfA ")) is finite Element of bool NAT

dom sfA is finite Element of bool NAT

len z is V9() V10() V11() V15() finite cardinal Element of NAT

Y is set

i is set

dom (T,sfA,z) is finite Element of bool NAT

i is V9() V10() V11() V15() finite cardinal set

(T,sfA,z) . i is set

(sfA * (sfA ")) . i is set

j is V9() V10() V11() V15() finite cardinal Element of NAT

a . j is boolean set

((sfA * (sfA ")) * a) . i is set

z . i is boolean set

[:(dom sfA),(rng sfA):] is Relation-like finite set

bool [:(dom sfA),(rng sfA):] is non empty finite V31() set

(T,sfA,a) . j is set

sfA . j is set

(sfA * (sfA ")) * sfA is Relation-like NAT -defined bool T -valued Function-like finite set

((sfA * (sfA ")) * sfA) . i is set

(sfA ") * sfA is Relation-like bool T -valued Function-like set

sfA * ((sfA ") * sfA) is Relation-like NAT -defined bool T -valued Function-like finite set

(sfA * ((sfA ") * sfA)) . i is set

id (rng sfA) is Relation-like rng sfA -defined rng sfA -valued Function-like one-to-one set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

sfA . i is set

(T,sfA,a) . j is set

sfA . j is set

T \ (sfA . j) is Element of bool T

(sfA * (sfA ")) * sfA is Relation-like NAT -defined bool T -valued Function-like finite set

((sfA * (sfA ")) * sfA) . i is set

T \ (((sfA * (sfA ")) * sfA) . i) is Element of bool T

(sfA ") * sfA is Relation-like bool T -valued Function-like set

sfA * ((sfA ") * sfA) is Relation-like NAT -defined bool T -valued Function-like finite set

(sfA * ((sfA ") * sfA)) . i is set

T \ ((sfA * ((sfA ") * sfA)) . i) is Element of bool T

id (rng sfA) is Relation-like rng sfA -defined rng sfA -valued Function-like one-to-one set

sfA * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(sfA * (id (rng sfA))) . i is set

T \ ((sfA * (id (rng sfA))) . i) is Element of bool T

sfA . i is set

T \ (sfA . i) is Element of bool T

(T,sfA,a) . j is set

(T,sfA,a) . j is set

dom (T,sfA,a) is finite Element of bool NAT

T is set

bool T is non empty set

bool (bool T) is non empty set

tT is finite Element of bool (bool T)

(T,tT) is finite Element of bool (bool T)

union (T,tT) is Element of bool T

B is set

bool T is non empty Element of bool (bool T)

card tT is V9() V10() V11() V15() finite cardinal Element of NAT

x is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len x is V9() V10() V11() V15() finite cardinal Element of NAT

rng x is finite Element of bool (bool T)

bool (bool T) is non empty set

{ (Intersect (rng (T,x,b

Seg (len x) is finite len x -element Element of bool NAT

sfA is V9() V10() V11() V15() finite cardinal set

x . sfA is set

sfA is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

sfA is set

(T,x,sfA) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,x,sfA) is finite Element of bool (bool T)

dom (T,x,sfA) is finite Element of bool NAT

a is V9() V10() V11() V15() finite cardinal set

(T,x,sfA) . a is set

dom x is finite Element of bool NAT

x . a is set

sfA . a is boolean set

x . a is set

sfA . a is boolean set

T \ (x . a) is Element of bool T

x . a is set

Intersect (rng (T,x,sfA)) is Element of bool T

T is set

bool T is non empty set

bool (bool T) is non empty set

tT is finite Element of bool (bool T)

(T,tT) is finite Element of bool (bool T)

B is set

x is set

B /\ x is set

sfA is set

bool T is non empty Element of bool (bool T)

card tT is V9() V10() V11() V15() finite cardinal Element of NAT

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

rng sfA is finite Element of bool (bool T)

bool (bool T) is non empty set

{ (Intersect (rng (T,sfA,b

a is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

(T,sfA,a) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,sfA,a) is finite Element of bool (bool T)

Intersect (rng (T,sfA,a)) is Element of bool T

len a is V9() V10() V11() V15() finite cardinal Element of NAT

z is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

(T,sfA,z) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,sfA,z) is finite Element of bool (bool T)

Intersect (rng (T,sfA,z)) is Element of bool T

len z is V9() V10() V11() V15() finite cardinal Element of NAT

len (T,sfA,a) is V9() V10() V11() V15() finite cardinal Element of NAT

dom (T,sfA,a) is finite Element of bool NAT

Seg (len sfA) is finite len sfA -element Element of bool NAT

y1 is V9() V10() V11() V15() finite cardinal set

dom sfA is finite Element of bool NAT

(T,sfA,a) . y1 is set

dom (T,sfA,z) is finite Element of bool NAT

(T,sfA,z) . y1 is set

a . y1 is boolean set

sfA . y1 is set

z . y1 is boolean set

T \ (sfA . y1) is Element of bool T

a . y1 is boolean set

sfA . y1 is set

T \ (sfA . y1) is Element of bool T

z . y1 is boolean set

a . y1 is boolean set

len (T,sfA,z) is V9() V10() V11() V15() finite cardinal Element of NAT

T is set

bool T is non empty set

bool (bool T) is non empty set

T is set

bool T is non empty set

bool (bool T) is non empty set

B is finite Element of bool (bool T)

tT is finite Element of bool (bool T)

(T,B) is finite Element of bool (bool T)

(T,tT) is finite Element of bool (bool T)

bool T is non empty Element of bool (bool T)

card tT is V9() V10() V11() V15() finite cardinal Element of NAT

x is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len x is V9() V10() V11() V15() finite cardinal Element of NAT

rng x is finite Element of bool (bool T)

bool (bool T) is non empty set

{ (Intersect (rng (T,x,b

x " is Relation-like Function-like set

dom (x ") is set

card B is V9() V10() V11() V15() finite cardinal Element of NAT

sfA is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

rng sfA is finite Element of bool (bool T)

{ (Intersect (rng (T,sfA,b

sfA is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

(T,x,sfA) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,x,sfA) is finite Element of bool (bool T)

Intersect (rng (T,x,sfA)) is Element of bool T

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT

(x ") * sfA is Relation-like BOOLEAN -valued Function-like set

sfA * ((x ") * sfA) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

dom x is finite Element of bool NAT

rng (x ") is set

Seg (len sfA) is finite len sfA -element Element of bool NAT

a is V9() V10() V11() V15() finite cardinal set

sfA . a is set

(sfA * ((x ") * sfA)) . a is set

dom sfA is finite Element of bool NAT

dom sfA is finite Element of bool NAT

dom ((x ") * sfA) is set

((x ") * sfA) . (sfA . a) is set

rng ((x ") * sfA) is Element of bool BOOLEAN

bool BOOLEAN is non empty set

rng (sfA * ((x ") * sfA)) is finite Element of bool BOOLEAN

a is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN

len a is V9() V10() V11() V15() finite cardinal Element of NAT

sfA " is Relation-like Function-like set

dom (sfA ") is set

(T,sfA,a) is Relation-like NAT -defined bool T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool T

rng (T,sfA,a) is finite Element of bool (bool T)

z is set

dom (T,x,sfA) is finite Element of bool NAT

y1 is V9() V10() V11() V15() finite cardinal set

(T,x,sfA) . y1 is set

len (T,x,sfA) is V9() V10() V11() V15() finite cardinal Element of NAT

Seg (len (T,x,sfA)) is finite len (T,x,sfA) -element Element of bool NAT

Seg (len x) is finite len x -element Element of bool NAT

x * (sfA ") is Relation-like NAT -defined Function-like finite set

dom (x * (sfA ")) is finite Element of bool NAT

(x * (sfA ")) . y1 is set

rng (x * (sfA ")) is finite set

rng (sfA ") is set

dom sfA is finite Element of bool NAT

Y is V9() V10() V11() V15() finite cardinal Element of NAT

sfA . Y is set

(x * (sfA ")) * sfA is Relation-like NAT -defined bool T -valued Function-like finite set

((x * (sfA ")) * sfA) . y1 is set

(sfA ") * sfA is Relation-like bool T -valued Function-like set

x * ((sfA ") * sfA) is Relation-like NAT -defined bool T -valued Function-like finite set

(x * ((sfA ") * sfA)) . y1 is set

id (rng sfA) is Relation-like rng sfA -defined rng sfA -valued Function-like one-to-one set

x * (id (rng sfA)) is Relation-like NAT -defined rng sfA -valued Function-like finite set

(x * (id (rng sfA))) . y1 is set

x . y1 is set

a . Y is boolean set

(sfA * ((x ") * sfA)) . ((x * (sfA ")) . y1) is set

(x * (sfA ")) * (sfA * ((x ") * sfA)) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

((x * (sfA ")) * (sfA * ((x ") * sfA))) . y1 is set

((x * (sfA ")) * sfA) * ((x ") * sfA) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(((x * (sfA ")) * sfA) * ((x ") * sfA)) . y1 is set

(x * ((sfA ") * sfA)) * ((x ") * sfA) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

((x * ((sfA ") * sfA)) * ((x ") * sfA)) . y1 is set

(x * (id (rng sfA))) * ((x ") * sfA) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

((x * (id (rng sfA))) * ((x ") * sfA)) . y1 is set

x * ((x ") * sfA) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

(x * ((x ") * sfA)) . y1 is set

x * (x ") is Relation-like NAT -defined Function-like finite set

(x * (x ")) * sfA is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

((x * (x ")) * sfA) . y1 is set

id (dom x) is Relation-like dom x -defined dom x -valued Function-like one-to-one set

(id (dom x)) * sfA is Relation-like dom x -defined BOOLEAN -valued Function-like set

((id (dom x)) * sfA) . y1 is set

dom sfA is finite Element of bool NAT

id (dom sfA) is Relation-like dom sfA -defined dom sfA -valued Function-like one-to-one set

(id (dom sfA)) * sfA is Relation-like dom sfA -defined BOOLEAN -valued Function-like set

((id (dom sfA)) * sfA) . y1 is set

sfA . y1 is boolean set

(T,sfA,a) . Y is set

T \ (x . y1) is Element of bool T

T \ ((x * (id (rng sfA))) . y1) is Element of bool T

T \ ((x * ((sfA ") * sfA)) . y1) is Element of bool T

T \ (((x * (sfA ")) * sfA) . y1) is Element of bool T

T \ (sfA . Y) is Element of bool T

(T,sfA,a) . Y is set

(T,sfA,a) . Y is set

(T,sfA,a) . Y is set

dom (T,sfA,a) is finite Element of bool NAT

Intersect (rng (T,sfA,a)) is Element of bool T

T is non empty set

bool T is non empty set

bool (bool T) is non empty set

tT is Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() Function-like one-to-one constant functional empty trivial proper finite finite-yielding V31() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of bool (bool T)

{T} is non empty trivial finite 1 -element set

(T,tT) is finite Element of bool (bool T)

T is non empty set

bool T is non empty set

bool (bool T) is non empty set

tT is finite Element of bool (bool T)

(T,tT) is finite Element of bool (bool T)

B is Element of bool T

x is Element of bool T

union (T,tT) is Element of bool T

T is non empty RelStr

[#] T is non empty non proper lower upper Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T is non empty set

bool ([#] T) is non empty set

tT is Element of bool ([#] T)

"/\" (tT,T) is Element of the carrier of T

tT is Element of bool ([#] T)

"\/" (tT,T) is Element of the carrier of T

T is non empty RelStr

[#] T is non empty non proper lower upper Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T is non empty set

Bottom T is Element of the carrier of T

Top T is Element of the carrier of T

T is non empty RelStr

[#] T is non empty non proper lower upper Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T is non empty set

T is non empty V102() V103() V104() upper-bounded V150() up-complete satisfying_axiom_of_approximation continuous RelStr

[#] T is non empty non proper directed lower upper meet-closed join-closed infs-closed sups-closed with_bottom with_top Element of bool the carrier of T

the carrier of T is non empty set

bool the carrier of T is non empty set

tT is Element of the carrier of T

waybelow tT is non empty directed lower join-closed Element of bool the carrier of T

(waybelow tT) /\ ([#] T) is Element of bool the carrier of T

"\/" (((waybelow tT) /\ ([#] T)),T) is Element of the carrier of T

T is non empty V102() V103() V104() up-complete RelStr

the carrier of T is non empty set

CompactSublatt T is strict V109(T) SubRelStr of T

the carrier of (CompactSublatt T) is set

tT is set

B is Element of the carrier of T

T is non empty V102() V103() V104() lower-bounded V150() RelStr

the carrier of T is non empty set

bool the carrier of T is non empty set

tT is Element of bool the carrier of T

card tT is V9() V10() V11() cardinal set

finsups tT is non empty directed Element of bool the carrier of T

card (finsups tT) is V9() V10() V11() non empty cardinal set

B is non empty Element of bool the carrier of T

B * is functional non empty FinSequence-membered FinSequenceSet of B

finsups B is non empty directed Element of bool the carrier of T

x is Relation-like NAT -defined B -valued Function-like finite FinSequence-like FinSubsequence-like Element of B *

rng x is finite set

"\/" ((rng x),T) is Element of the carrier of T

rng x is finite Element of bool B

bool B is non empty set

"\/" ((rng x),T) is Element of the carrier of T

{ ("\/" (b

sfA is Element of finsups B

[:(B *),(finsups B):] is Relation-like non empty set

bool [:(B *),(finsups B):] is non empty set

x is Relation-like B * -defined finsups B -valued Function-like V39(B * , finsups B) Element of bool [:(B *),(finsups B):]

sfA is set

sfA is Element of the carrier of T

{sfA} is non empty trivial finite 1 -element Element of bool the carrier of T

a is set

"\/" ({sfA},T) is Element of the carrier of T

bool tT is non empty set

{ ("\/" (b

dom x is functional FinSequence-membered Element of bool (B *)

bool (B *) is non empty set

rng x is Element of bool (finsups B)

bool (finsups B) is non empty set

sfA is set

bool tT is non empty set

{ ("\/" (b

sfA is finite Element of bool tT

"\/" (sfA,T) is Element of the carrier of T

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng a is finite set

z is Relation-like NAT -defined B -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of B

y1 is Relation-like NAT -defined B -valued Function-like finite FinSequence-like FinSubsequence-like Element of B *

x . y1 is Element of finsups B

rng y1 is finite Element of bool B

bool B is non empty set

"\/" ((rng y1),T) is Element of the carrier of T

card (finsups B) is V9() V10() V11() non empty cardinal set

card (B *) is V9() V10() V11() non empty cardinal set

card B is V9() V10() V11() non empty cardinal set

T is non empty TopSpace-like T_0 TopStruct

the carrier of T is non empty set

card the carrier of T is V9() V10() V11() non empty cardinal set

the topology of T is non empty Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

card the topology of T is V9() V10() V11() non empty cardinal set

[#] T is non empty non proper open closed Element of bool the carrier of T

tT is Element of the carrier of T

{tT} is non empty trivial finite 1 -element Element of bool the carrier of T

Cl {tT} is closed Element of bool the carrier of T

([#] T) \ (Cl {tT}) is Element of bool the carrier of T

B is Element of the topology of T

[: the carrier of T, the topology of T:] is Relation-like non empty set

bool [: the carrier of T, the topology of T:] is non empty set

tT is Relation-like the carrier of T -defined the topology of T -valued Function-like V39( the carrier of T, the