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
F1() is V9() V10() V11() V15() finite cardinal set
Seg F1() is finite F1() -element Element of bool NAT
F2() is non empty set
T is set
F3(T) is set
F4(T) is set
[:(Seg F1()),F2():] is Relation-like set
bool [:(Seg F1()),F2():] is non empty set
T is Relation-like Seg F1() -defined F2() -valued Function-like finite V39( Seg F1(),F2()) Element of bool [:(Seg F1()),F2():]
dom T is finite Element of bool (Seg F1())
bool (Seg F1()) is non empty finite V31() set
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 F2() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of F2()
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
F3(x) is set
F4(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
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of BOOLEAN : len b1 = len tT } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len x } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len sfA } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len sfA } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len sfA } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len sfA } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len B } is set
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
{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = len B } is set
{ (Intersect (rng (T,B,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued Element of BOOLEAN * : b1 in (len B) -tuples_on BOOLEAN } is set
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
{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like Element of BOOLEAN * : len b1 = len sfA } is set
{ H1(b1) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued Element of BOOLEAN * : b1 in (len B) -tuples_on BOOLEAN } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len B } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len sfA } 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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len sfA } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len x } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len sfA } 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
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len x } is set
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,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len sfA } is set
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
{ ("\/" (b1,T)) where b1 is finite Element of bool B : ex_sup_of b1,T } is set
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
{ ("\/" (b1,T)) where b1 is finite Element of bool tT : ex_sup_of b1,T } is set
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
{ ("\/" (b1,T)) where b1 is finite Element of bool tT : ex_sup_of b1,T } is set
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 topology of T) Element of bool [: the carrier of T, the topology of T:]
B is set
dom tT is set
x is set
tT . B is set
tT . x is set
dom tT is Element of bool the carrier of T
sfA is Element of the carrier of T
{sfA} is non empty trivial finite 1 -element Element of bool the carrier of T
Cl {sfA} is closed Element of bool the carrier of T
(Cl {sfA}) ` is open Element of bool the carrier of T
([#] T) \ (Cl {sfA}) is Element of bool the carrier of T
sfA is Element of the carrier of T
{sfA} is non empty trivial finite 1 -element Element of bool the carrier of T
Cl {sfA} is closed Element of bool the carrier of T
([#] T) \ (Cl {sfA}) is Element of bool the carrier of T
(Cl {sfA}) ` is open Element of bool the carrier of T
dom tT is Element of bool the carrier of T
rng tT is Element of bool the topology of T
bool the topology of T is non empty set
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
tT is Element of bool the carrier of T
the topology of T is Element of bool (bool the carrier of T)
B is finite Element of bool (bool the carrier of T)
( the carrier of T,B) is finite Element of bool (bool the carrier of T)
UniCl B is Element of bool (bool the carrier of T)
x is Element of bool (bool the carrier of T)
union x is Element of bool the carrier of T
sfA is set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
card B is V9() V10() V11() V15() finite cardinal Element of NAT
sfA is Relation-like NAT -defined bool the carrier of T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of T
len sfA is V9() V10() V11() V15() finite cardinal Element of NAT
rng sfA is finite Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
{ (Intersect (rng ( the carrier of T,sfA,b1))) where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN : len b1 = len sfA } is set
a is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like boolean-valued FinSequence of BOOLEAN
( the carrier of T,sfA,a) is Relation-like NAT -defined bool the carrier of T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of T
rng ( the carrier of T,sfA,a) is finite Element of bool (bool the carrier of T)
Intersect (rng ( the carrier of T,sfA,a)) is Element of bool the carrier of T
len a is V9() V10() V11() V15() finite cardinal Element of NAT
tT /\ sfA is Element of bool the carrier of T
z is set
y1 is set
Y is set
dom sfA is finite Element of bool NAT
i is V9() V10() V11() V15() finite cardinal set
sfA . i is set
dom ( the carrier of T,sfA,a) is finite Element of bool NAT
a . i is boolean set
( the carrier of T,sfA,a) . i is set
a . i is boolean set
( the carrier of T,sfA,a) . i is set
the carrier of T \ y1 is Element of bool the carrier of T
a . i is boolean set
( the carrier of T,sfA,a) . i is set
( the carrier of T,sfA,a) . i is set
T is TopSpace-like T_0 TopStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
tT is open quasi_basis Element of bool (bool the carrier of T)
B is finite Element of bool (bool the carrier of T)
( the carrier of T,B) is finite Element of bool (bool the carrier of T)
union ( the carrier of T,B) is Element of bool the carrier of T
x is set
sfA is non empty non trivial non finite set
sfA is set
a is set
z is Element of the carrier of T
y1 is Element of the carrier of T
Y is Element of bool the carrier of T
Y /\ sfA is Element of bool the carrier of T
Y /\ sfA is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
the topology of T is non empty Element of bool (bool the carrier of T)
B is open quasi_basis Element of bool (bool the carrier of T)
x is Element of the carrier of T
{ b1 where b1 is Element of the topology of T : x in b1 } is set
meet { b1 where b1 is Element of the topology of T : x in b1 } is set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
sfA is set
sfA is Element of the topology of T
sfA is Element of bool (bool the carrier of T)
a is set
sfA is Element of bool (bool the carrier of T)
z is Element of the topology of T
meet sfA is Element of bool the carrier of T
a is Element of bool the carrier of T
z is Element of the topology of T
tT is non empty finite set
{ H1(b1) where b1 is Element of tT : S1[b1] } is set
a is Element of bool the carrier of T
z is set