:: 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

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

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

rng tT is finite set

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

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

len x is V9() V10() V11() V15() finite cardinal Element of 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

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

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

len sfA is V9() V10() V11() V15() finite cardinal Element of 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

dom tT is finite Element of bool NAT

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

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

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

dom tT is finite Element of bool NAT

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

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

len (T,(<*> (bool T)),tT) is V9() V10() V11() V15() finite cardinal 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

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

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

T is set
bool T is non empty set
tT is Element 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

T \ tT is Element of bool T

B . 1 is set

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

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

T \ tT is Element of bool T
T \ B is Element of bool T

x . 1 is set

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

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

T \ tT is Element of bool T
T \ B is Element of bool T
T \ x is Element of bool T

sfA . 1 is set

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

len tT is V9() V10() V11() V15() finite cardinal Element of NAT
{ } is set
B is set

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

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

rng B is finite set

len x is V9() V10() V11() V15() finite cardinal Element of NAT
{ } 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)

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
{ } is set

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
{ } is set

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT
rng sfA is finite Element of bool (bool T)
{ } is set

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT
rng sfA is finite Element of bool (bool T)
{ } 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

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

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

[:(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 * ((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

dom (sfA ") is set

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

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 * ((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

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 ")) * z is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

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

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

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

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

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

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

[:(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 * ((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

dom (sfA ") is set

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

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 * ((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

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 ")) * z is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

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

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

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

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

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
{ } is set

{ } is set
{ } is set
x is set

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

{ } is set
{ } 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

(T,tT) is finite Element of bool (bool T)
bool T is non empty Element of bool (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
{ } is set
x is set

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

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

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

is Relation-like non empty non trivial non finite set

rng (T,B,()) is finite Element of bool (bool T)
Intersect (rng (T,B,())) 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

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
{ } is set
card B is V9() V10() V11() V15() finite cardinal Element of NAT

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT
rng sfA is finite Element of bool (bool T)
{ } is set
x is set

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 sfA),BOOLEAN:] is Relation-like set
bool [:(dom sfA),BOOLEAN:] is non empty set

dom (sfA ") is set
rng (sfA ") is 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 * ((sfA ") * a) is Relation-like NAT -defined BOOLEAN -valued Function-like finite set

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

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

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

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
{ } is set

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

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

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

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

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
{ } is set

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

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

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
{ } is set

dom (x ") is set
card B is V9() V10() V11() V15() finite cardinal Element of NAT

len sfA is V9() V10() V11() V15() finite cardinal Element of NAT
rng sfA is finite Element of bool (bool T)
{ } is set

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

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

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

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

dom (sfA ") is set

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

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

(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)) . y1 is set

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

((id (dom x)) * sfA) . y1 is set
dom sfA is finite Element of bool NAT

(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

{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

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 () 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

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

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 *),():] is Relation-like non empty set
bool [:(B *),():] is non empty set
x is Relation-like B * -defined finsups B -valued Function-like V39(B * , finsups B) Element of bool [:(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

bool (B *) is non empty set
rng x is Element of bool ()
bool () 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

rng a is finite set

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 () 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