REAL is non empty V36() V66() V67() V68() V72() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V66() V67() V68() V69() V70() V71() V72() Element of K6(REAL)
K6(REAL) is non empty set
ExtREAL is non empty V67() set
K7(NAT,ExtREAL) is non empty V74() set
K6(K7(NAT,ExtREAL)) is non empty set
K6(ExtREAL) is non empty set
K471() is TopSpace-like V186() SubSpace of R^1
R^1 is non empty strict TopSpace-like V186() TopStruct
the carrier of K471() is V66() V67() V68() set
K449(K471(),K471()) is strict TopSpace-like TopStruct
the carrier of K449(K471(),K471()) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V66() V67() V68() V69() V70() V71() V72() set
K6(omega) is non empty set
K7(NAT,REAL) is non empty V73() V74() V75() set
K6(K7(NAT,REAL)) is non empty set
K6(K6(REAL)) is non empty set
COMPLEX is non empty V36() V66() V72() set
K6(NAT) is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
INT is non empty V36() V66() V67() V68() V69() V70() V72() set
K7(1,1) is non empty RAT -valued INT -valued V73() V74() V75() V76() set
RAT is non empty V36() V66() V67() V68() V69() V72() set
K6(K7(1,1)) is non empty set
K7(K7(1,1),1) is non empty RAT -valued INT -valued V73() V74() V75() V76() set
K6(K7(K7(1,1),1)) is non empty set
K7(K7(1,1),REAL) is non empty V73() V74() V75() set
K6(K7(K7(1,1),REAL)) is non empty set
K7(REAL,REAL) is non empty V73() V74() V75() set
K7(K7(REAL,REAL),REAL) is non empty V73() V74() V75() set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
K7(2,2) is non empty RAT -valued INT -valued V73() V74() V75() V76() set
K7(K7(2,2),REAL) is non empty V73() V74() V75() set
K6(K7(K7(2,2),REAL)) is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V66() V67() V68() V69() V70() V71() V72() set
{{},1} is non empty V66() V67() V68() V69() V70() V71() set
K464() is V186() TopStruct
the carrier of K464() is V66() V67() V68() set
RealSpace is non empty strict Reflexive discerning V170() triangle Discerning V186() MetrStruct
K7( the carrier of K471(), the carrier of K471()) is V73() V74() V75() set
K6(K7( the carrier of K471(), the carrier of K471())) is non empty set
K6( the carrier of K449(K471(),K471())) is non empty set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V61() V66() V67() V68() V69() V70() V71() V72() Element of NAT
the carrier of RealSpace is non empty V66() V67() V68() set
TopSpaceMetr RealSpace is TopStruct
the carrier of R^1 is non empty V66() V67() V68() set
DYADIC is non empty V66() V67() V68() Element of K6(REAL)
DOM is non empty V66() V67() V68() Element of K6(REAL)
halfline 0 is V66() V67() V68() Element of K6(REAL)
-infty is non empty non real ext-real non positive negative set
].-infty,0.[ is set
(halfline 0) \/ DYADIC is non empty V66() V67() V68() Element of K6(REAL)
right_open_halfline 1 is V66() V67() V68() Element of K6(REAL)
+infty is non empty non real ext-real positive non negative set
].1,+infty.[ is set
((halfline 0) \/ DYADIC) \/ (right_open_halfline 1) is non empty V66() V67() V68() Element of K6(REAL)
dyadic 0 is non empty V66() V67() V68() Element of K6(REAL)
K428(REAL,0,1) is non empty V66() V67() V68() V69() V70() V71() Element of K6(REAL)
[.0,1.] is set
DYADIC \/ (right_open_halfline 1) is non empty V66() V67() V68() Element of K6(REAL)
real_dist is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like V33(K7(REAL,REAL), REAL ) V73() V74() V75() Element of K6(K7(K7(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
K7((dyadic 0),(bool the carrier of T)) is non empty set
K6(K7((dyadic 0),(bool the carrier of T))) is non empty set
[#] T is non empty non proper closed Element of K6( the carrier of T)
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
([#] T) \ B is Element of K6( the carrier of T)
S is Element of K6( the carrier of T)
B ` is Element of K6( the carrier of T)
A \ B is Element of K6( the carrier of T)
L is Element of K6( the carrier of T)
Cl L is Element of K6( the carrier of T)
r is V11() real ext-real Element of dyadic 0
r is Relation-like dyadic 0 -defined bool the carrier of T -valued Function-like V33( dyadic 0, bool the carrier of T) Element of K6(K7((dyadic 0),(bool the carrier of T)))
r is Relation-like dyadic 0 -defined bool the carrier of T -valued Function-like V33( dyadic 0, bool the carrier of T) Element of K6(K7((dyadic 0),(bool the carrier of T)))
x is V11() real ext-real Element of dyadic 0
F is V11() real ext-real Element of dyadic 0
r . F is Element of K6( the carrier of T)
r . x is Element of K6( the carrier of T)
Cl (r . F) is Element of K6( the carrier of T)
r . 1 is set
r . 0 is set
r . 1 is set
([#] T) \ (r . 1) is Element of K6( the carrier of T)
x is V11() real ext-real Element of dyadic 0
F is V11() real ext-real Element of dyadic 0
r . F is Element of K6( the carrier of T)
r . x is Element of K6( the carrier of T)
Cl (r . F) is Element of K6( the carrier of T)
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
[#] T is non empty non proper closed Element of K6( the carrier of T)
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic S is non empty V66() V67() V68() Element of K6(REAL)
K7((dyadic S),(bool the carrier of T)) is non empty set
K6(K7((dyadic S),(bool the carrier of T))) is non empty set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (S + 1) is non empty V66() V67() V68() Element of K6(REAL)
K7((dyadic (S + 1)),(bool the carrier of T)) is non empty set
K6(K7((dyadic (S + 1)),(bool the carrier of T))) is non empty set
L is Relation-like dyadic S -defined bool the carrier of T -valued Function-like V33( dyadic S, bool the carrier of T) Element of K6(K7((dyadic S),(bool the carrier of T)))
L . 0 is set
L . 1 is set
([#] T) \ (L . 1) is Element of K6( the carrier of T)
r is Relation-like dyadic (S + 1) -defined bool the carrier of T -valued Function-like V33( dyadic (S + 1), bool the carrier of T) Element of K6(K7((dyadic (S + 1)),(bool the carrier of T)))
r . 0 is set
r . 1 is set
([#] T) \ (r . 1) is Element of K6( the carrier of T)
x is V11() real ext-real Element of dyadic (S + 1)
F is V11() real ext-real Element of dyadic (S + 1)
r . F is Element of K6( the carrier of T)
r . x is Element of K6( the carrier of T)
Cl (r . F) is Element of K6( the carrier of T)
K7((dyadic 0),(bool the carrier of T)) is non empty set
K6(K7((dyadic 0),(bool the carrier of T))) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
A is Element of K6( the carrier of T)
B is Element of K6( the carrier of T)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic S is non empty V66() V67() V68() Element of K6(REAL)
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
K7((dyadic S),(bool the carrier of T)) is non empty set
K6(K7((dyadic S),(bool the carrier of T))) is non empty set
[#] T is non empty non proper closed Element of K6( the carrier of T)
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic S is non empty V66() V67() V68() Element of K6(REAL)
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (S + 1) is non empty V66() V67() V68() Element of K6(REAL)
L is Relation-like dyadic S -defined bool the carrier of T -valued Function-like V33( dyadic S, bool the carrier of T) (T,A,B,S)
F is V11() real ext-real Element of dyadic S
r is V11() real ext-real Element of dyadic S
L . r is Element of K6( the carrier of T)
L . F is Element of K6( the carrier of T)
Cl (L . r) is Element of K6( the carrier of T)
L . 0 is set
[#] T is non empty non proper closed Element of K6( the carrier of T)
L . 1 is set
([#] T) \ (L . 1) is Element of K6( the carrier of T)
K7((dyadic (S + 1)),(bool the carrier of T)) is non empty set
K6(K7((dyadic (S + 1)),(bool the carrier of T))) is non empty set
r is Relation-like dyadic (S + 1) -defined bool the carrier of T -valued Function-like V33( dyadic (S + 1), bool the carrier of T) Element of K6(K7((dyadic (S + 1)),(bool the carrier of T)))
r . 0 is set
r . 1 is set
([#] T) \ (r . 1) is Element of K6( the carrier of T)
x is V11() real ext-real Element of dyadic (S + 1)
F is V11() real ext-real Element of dyadic (S + 1)
r . F is Element of K6( the carrier of T)
r . x is Element of K6( the carrier of T)
Cl (r . F) is Element of K6( the carrier of T)
F is Relation-like dyadic (S + 1) -defined bool the carrier of T -valued Function-like V33( dyadic (S + 1), bool the carrier of T) (T,A,B,S + 1)
x is V11() real ext-real Element of dyadic (S + 1)
F . x is Element of K6( the carrier of T)
L . x is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is Element of K6( the carrier of T)
B is Element of K6( the carrier of T)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic S is non empty V66() V67() V68() Element of K6(REAL)
L is Relation-like dyadic S -defined bool the carrier of T -valued Function-like V33( dyadic S, bool the carrier of T) (T,A,B,S)
K7(DYADIC,(bool the carrier of T)) is non empty set
K6(K7(DYADIC,(bool the carrier of T))) is non empty set
T is non empty set
A is non empty set
PFuncs (T,A) is non empty functional set
K7(NAT,(PFuncs (T,A))) is non empty set
K6(K7(NAT,(PFuncs (T,A)))) is non empty set
B is Relation-like NAT -defined PFuncs (T,A) -valued Function-like V33( NAT , PFuncs (T,A)) Element of K6(K7(NAT,(PFuncs (T,A))))
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
B . S is Relation-like Function-like set
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
K7(NAT,(PFuncs (DYADIC,(bool the carrier of T)))) is non empty set
K6(K7(NAT,(PFuncs (DYADIC,(bool the carrier of T))))) is non empty set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is set
the Relation-like dyadic 0 -defined bool the carrier of T -valued Function-like V33( dyadic 0, bool the carrier of T) (T,A,B, 0 ) is Relation-like dyadic 0 -defined bool the carrier of T -valued Function-like V33( dyadic 0, bool the carrier of T) (T,A,B, 0 )
r is non empty set
K7(DYADIC,(bool the carrier of T)) is non empty set
K6(K7(DYADIC,(bool the carrier of T))) is non empty set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
O2 is Element of r
P is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic P is non empty V66() V67() V68() Element of K6(REAL)
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (P + 1) is non empty V66() V67() V68() Element of K6(REAL)
r0 is Relation-like dyadic P -defined bool the carrier of T -valued Function-like V33( dyadic P, bool the carrier of T) (T,A,B,P)
r1 is Relation-like dyadic (P + 1) -defined bool the carrier of T -valued Function-like V33( dyadic (P + 1), bool the carrier of T) (T,A,B,P + 1)
dom r0 is set
n is Element of dom r0
r0 . n is set
r1 . n is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic n is non empty V66() V67() V68() Element of K6(REAL)
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (n + 1) is non empty V66() V67() V68() Element of K6(REAL)
2 |^ P is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
1 / (2 |^ P) is V11() real ext-real non negative Element of REAL
1 * (2 |^ P) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
2 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r1 / (2 |^ n) is V11() real ext-real non negative Element of REAL
1 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r1 * (2 |^ P) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(2 |^ n) / (2 |^ P) is V11() real ext-real non negative Element of REAL
H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
H + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(H + 1) - 1 is V11() real ext-real Element of REAL
2 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
1 / (2 |^ n) is V11() real ext-real non negative Element of REAL
1 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
2 |^ P is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r1 / (2 |^ P) is V11() real ext-real non negative Element of REAL
1 * (2 |^ P) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r1 * (2 |^ n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(2 |^ P) / (2 |^ n) is V11() real ext-real non negative Element of REAL
H is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
H + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(H + 1) - 1 is V11() real ext-real Element of REAL
n is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
r1 is Element of r
D is Element of r
x is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
dom x is set
H is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic r1 is non empty V66() V67() V68() Element of K6(REAL)
r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (r1 + 1) is non empty V66() V67() V68() Element of K6(REAL)
r2 is Element of dom x
x . r2 is set
H . r2 is set
x is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
r1 is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
H is Element of r
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic r2 is non empty V66() V67() V68() Element of K6(REAL)
dom x is set
H is Element of r
x is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
r1 is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic r2 is non empty V66() V67() V68() Element of K6(REAL)
dom x is set
K7(NAT,r) is non empty set
K6(K7(NAT,r)) is non empty set
F is Element of r
x is Relation-like NAT -defined r -valued Function-like V33( NAT ,r) Element of K6(K7(NAT,r))
x . 0 is Element of r
x is Relation-like NAT -defined r -valued Function-like V33( NAT ,r) Element of K6(K7(NAT,r))
x . 0 is Element of r
O2 is set
rng x is set
dom x is set
O2 is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) Element of K6(K7(NAT,(PFuncs (DYADIC,(bool the carrier of T)))))
P is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),O2,P) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
dyadic P is non empty V66() V67() V68() Element of K6(REAL)
dom (DYADIC,(bool the carrier of T),O2,P) is set
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),O2,(P + 1)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
dyadic (P + 1) is non empty V66() V67() V68() Element of K6(REAL)
dom (DYADIC,(bool the carrier of T),O2,(P + 1)) is set
(P + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),O2,((P + 1) + 1)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
x . P is Element of r
x . (P + 1) is Element of r
r0 is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
r1 is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic n is non empty V66() V67() V68() Element of K6(REAL)
dom r0 is set
r0 is Element of dom (DYADIC,(bool the carrier of T),O2,(P + 1))
(DYADIC,(bool the carrier of T),O2,(P + 1)) . r0 is set
(DYADIC,(bool the carrier of T),O2,((P + 1) + 1)) . r0 is set
x . ((P + 1) + 1) is Element of r
r1 is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
n is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
D is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic D is non empty V66() V67() V68() Element of K6(REAL)
dom r1 is set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
x . (0 + 1) is Element of r
(DYADIC,(bool the carrier of T),O2,0) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
dom (DYADIC,(bool the carrier of T),O2,0) is set
(DYADIC,(bool the carrier of T),O2,(0 + 1)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
P is Element of dom (DYADIC,(bool the carrier of T),O2,0)
(DYADIC,(bool the carrier of T),O2,0) . P is set
(DYADIC,(bool the carrier of T),O2,(0 + 1)) . P is set
r0 is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
r1 is Relation-like DYADIC -defined bool the carrier of T -valued Function-like Element of K6(K7(DYADIC,(bool the carrier of T)))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic n is non empty V66() V67() V68() Element of K6(REAL)
dom r0 is set
r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),O2,r0) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
dom (DYADIC,(bool the carrier of T),O2,r0) is set
P is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),O2,P) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
dyadic P is non empty V66() V67() V68() Element of K6(REAL)
r1 is Element of dom (DYADIC,(bool the carrier of T),O2,r0)
(DYADIC,(bool the carrier of T),O2,r0) . r1 is set
r0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),O2,(r0 + 1)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),O2,(r0 + 1)) . r1 is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
A is Element of K6( the carrier of T)
B is Element of K6( the carrier of T)
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
K7(NAT,(PFuncs (DYADIC,(bool the carrier of T)))) is non empty set
K6(K7(NAT,(PFuncs (DYADIC,(bool the carrier of T))))) is non empty set
T is V11() real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic A is non empty V66() V67() V68() Element of K6(REAL)
A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
dyadic A is non empty V66() V67() V68() Element of K6(REAL)
A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
dyadic A is non empty V66() V67() V68() Element of K6(REAL)
B is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (S + 1) is non empty V66() V67() V68() Element of K6(REAL)
dyadic S is non empty V66() V67() V68() Element of K6(REAL)
dyadic B is non empty V66() V67() V68() Element of K6(REAL)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (S + 1) is non empty V66() V67() V68() Element of K6(REAL)
dyadic S is non empty V66() V67() V68() Element of K6(REAL)
A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic S is non empty V66() V67() V68() Element of K6(REAL)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
dyadic S is non empty V66() V67() V68() Element of K6(REAL)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
dyadic S is non empty V66() V67() V68() Element of K6(REAL)
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic r is non empty V66() V67() V68() Element of K6(REAL)
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
T is V11() real ext-real Element of REAL
(T) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (T) is non empty V66() V67() V68() Element of K6(REAL)
(T) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
B is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic B is non empty V66() V67() V68() Element of K6(REAL)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
((T) + 1) + S is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (((T) + 1) + S) is non empty V66() V67() V68() Element of K6(REAL)
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
((T) + 1) + (S + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (((T) + 1) + (S + 1)) is non empty V66() V67() V68() Element of K6(REAL)
(((T) + 1) + S) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic ((((T) + 1) + S) + 1) is non empty V66() V67() V68() Element of K6(REAL)
(T) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
S + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(T) + (S + 2) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(T) + L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
((T) + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (((T) + 1) + 0) is non empty V66() V67() V68() Element of K6(REAL)
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
((T) + 1) + r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (((T) + 1) + r) is non empty V66() V67() V68() Element of K6(REAL)
T is V11() real ext-real Element of REAL
(T) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (T) is non empty V66() V67() V68() Element of K6(REAL)
A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic A is non empty V66() V67() V68() Element of K6(REAL)
T is V11() real ext-real Element of REAL
(T) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic A is non empty V66() V67() V68() Element of K6(REAL)
B is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
dyadic B is non empty V66() V67() V68() Element of K6(REAL)
B is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
dyadic B is non empty V66() V67() V68() Element of K6(REAL)
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic L is non empty V66() V67() V68() Element of K6(REAL)
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
L + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
L is V11() real ext-real Element of REAL
(L) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),S,(L)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,(L)) . L is set
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(L) + F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),S,((L) + F)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,((L) + F)) . L is set
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(L) + (F + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),S,((L) + (F + 1))) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,((L) + (F + 1))) . L is set
((L) + F) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (((L) + F) + 1) is non empty V66() V67() V68() Element of K6(REAL)
dyadic ((L) + F) is non empty V66() V67() V68() Element of K6(REAL)
dom (DYADIC,(bool the carrier of T),S,((L) + F)) is set
(L) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),S,((L) + 0)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,((L) + 0)) . L is set
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(L) + F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),S,((L) + F)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,((L) + F)) . L is set
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
L is V11() real ext-real Element of REAL
(L) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(DYADIC,(bool the carrier of T),S,r) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
dyadic r is non empty V66() V67() V68() Element of K6(REAL)
(DYADIC,(bool the carrier of T),S,r) . L is set
F is Element of K6( the carrier of T)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic x is non empty V66() V67() V68() Element of K6(REAL)
(DYADIC,(bool the carrier of T),S,x) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,x) . L is set
O2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r + O2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
K7(DOM,(bool the carrier of T)) is non empty set
K6(K7(DOM,(bool the carrier of T))) is non empty set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
F is V11() real ext-real Element of DOM
L is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
x is Element of K6( the carrier of T)
L is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
r is ext-real Element of ExtREAL
x is Element of K6( the carrier of T)
x is ext-real Element of ExtREAL
r is ext-real Element of ExtREAL
x is Element of K6( the carrier of T)
L is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
L is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
r is V11() real ext-real Element of REAL
L . r is set
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic F is non empty V66() V67() V68() Element of K6(REAL)
(DYADIC,(bool the carrier of T),S,F) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,F) . r is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
A is Element of K6( the carrier of T)
B is Element of K6( the carrier of T)
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
K7(DOM,(bool the carrier of T)) is non empty set
K6(K7(DOM,(bool the carrier of T))) is non empty set
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
L is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
r is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
F is set
L . F is set
r . F is set
x is V11() real ext-real Element of REAL
L . x is set
L . x is set
O2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic O2 is non empty V66() V67() V68() Element of K6(REAL)
L . x is set
(DYADIC,(bool the carrier of T),S,O2) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,O2) . x is set
T is non empty set
A is TopSpace-like TopStruct
the carrier of A is set
bool the carrier of A is non empty Element of K6(K6( the carrier of A))
K6( the carrier of A) is non empty set
K6(K6( the carrier of A)) is non empty set
K7(T,(bool the carrier of A)) is non empty set
K6(K7(T,(bool the carrier of A))) is non empty set
B is Relation-like T -defined bool the carrier of A -valued Function-like V33(T, bool the carrier of A) Element of K6(K7(T,(bool the carrier of A)))
S is Element of T
B . S is set
B . S is Element of bool the carrier of A
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
(T,A,B,S) is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
K7(DOM,(bool the carrier of T)) is non empty set
K6(K7(DOM,(bool the carrier of T))) is non empty set
L is V11() real ext-real Element of REAL
(T,A,B,S) . L is set
r is Element of K6( the carrier of T)
the topology of T is non empty Element of K6(K6( the carrier of T))
F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic F is non empty V66() V67() V68() Element of K6(REAL)
(DYADIC,(bool the carrier of T),S,F) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
x is Relation-like dyadic F -defined bool the carrier of T -valued Function-like V33( dyadic F, bool the carrier of T) (T,A,B,F)
x . 0 is set
[#] T is non empty non proper closed Element of K6( the carrier of T)
x . 1 is set
([#] T) \ (x . 1) is Element of K6( the carrier of T)
P is V11() real ext-real Element of dyadic F
O2 is V11() real ext-real Element of dyadic F
((dyadic F),T,x,O2) is Element of K6( the carrier of T)
((dyadic F),T,x,P) is Element of K6( the carrier of T)
Cl ((dyadic F),T,x,O2) is Element of K6( the carrier of T)
(DYADIC,(bool the carrier of T),S,F) . L is set
O2 is V11() real ext-real Element of dyadic F
((dyadic F),T,x,O2) is Element of K6( the carrier of T)
the topology of T is non empty Element of K6(K6( the carrier of T))
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
(T,A,B,S) is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
K7(DOM,(bool the carrier of T)) is non empty set
K6(K7(DOM,(bool the carrier of T))) is non empty set
L is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
(T,A,B,S) . L is set
(T,A,B,S) . r is set
F is Element of K6( the carrier of T)
Cl F is Element of K6( the carrier of T)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic x is non empty V66() V67() V68() Element of K6(REAL)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic x is non empty V66() V67() V68() Element of K6(REAL)
O2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic O2 is non empty V66() V67() V68() Element of K6(REAL)
O2 + x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (O2 + x) is non empty V66() V67() V68() Element of K6(REAL)
(DYADIC,(bool the carrier of T),S,(O2 + x)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,(O2 + x)) . L is set
n is Relation-like dyadic (O2 + x) -defined bool the carrier of T -valued Function-like V33( dyadic (O2 + x), bool the carrier of T) (T,A,B,O2 + x)
r0 is V11() real ext-real Element of dyadic (O2 + x)
((dyadic (O2 + x)),T,n,r0) is Element of K6( the carrier of T)
Cl ((dyadic (O2 + x)),T,n,r0) is Element of K6( the carrier of T)
r1 is V11() real ext-real Element of dyadic (O2 + x)
((dyadic (O2 + x)),T,n,r1) is Element of K6( the carrier of T)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic x is non empty V66() V67() V68() Element of K6(REAL)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is Element of K6( the carrier of T)
B is Element of K6( the carrier of T)
L is Element of the carrier of T
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
(T,A,B,S) is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
K7(DOM,(bool the carrier of T)) is non empty set
K6(K7(DOM,(bool the carrier of T))) is non empty set
r is set
r is set
F is set
F is V67() Element of K6(ExtREAL)
x is set
O2 is V11() real ext-real Element of REAL
(T,A,B,S) . O2 is set
P is set
r is V67() Element of K6(ExtREAL)
F is V67() Element of K6(ExtREAL)
x is set
O2 is V11() real ext-real Element of REAL
(T,A,B,S) . O2 is set
O2 is V11() real ext-real Element of REAL
(T,A,B,S) . O2 is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is Element of K6( the carrier of T)
B is Element of K6( the carrier of T)
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
L is Element of the carrier of T
(T,A,B,S,L) is V67() Element of K6(ExtREAL)
r is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is Element of K6( the carrier of T)
B is Element of K6( the carrier of T)
K7( the carrier of T, the carrier of R^1) is non empty V73() V74() V75() set
K6(K7( the carrier of T, the carrier of R^1)) is non empty set
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
L is Element of the carrier of T
(T,A,B,S,L) is V67() Element of K6(ExtREAL)
r is V11() real ext-real Element of the carrier of R^1
F is non empty V67() Element of K6(ExtREAL)
sup F is ext-real Element of ExtREAL
r is non empty V67() Element of K6(ExtREAL)
x is set
0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V66() V67() V68() V69() V70() V71() V72() Element of ExtREAL
F is ext-real Element of ExtREAL
[.0.,F.] is set
inf r is ext-real Element of ExtREAL
sup r is ext-real Element of ExtREAL
O2 is ext-real Element of ExtREAL
P is V11() real ext-real Element of the carrier of R^1
r0 is non empty V67() Element of K6(ExtREAL)
sup r0 is ext-real Element of ExtREAL
L is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
L is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
r is Element of the carrier of T
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
L . r is V11() real ext-real Element of REAL
x is non empty V67() Element of K6(ExtREAL)
F is Element of the carrier of T
(T,A,B,S,F) is V67() Element of K6(ExtREAL)
L . F is V11() real ext-real Element of REAL
sup x is ext-real Element of ExtREAL
L is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
r is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
F is set
L . F is V11() real ext-real Element of REAL
r . F is V11() real ext-real Element of REAL
x is Element of the carrier of T
(T,A,B,S,x) is V67() Element of K6(ExtREAL)
L . x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
x is Element of the carrier of T
(T,A,B,S,x) is V67() Element of K6(ExtREAL)
L . x is V11() real ext-real Element of REAL
O2 is non empty V67() Element of K6(ExtREAL)
sup O2 is ext-real Element of ExtREAL
r . x is V11() real ext-real Element of REAL
x is Element of the carrier of T
(T,A,B,S,x) is V67() Element of K6(ExtREAL)
0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V66() V67() V68() V69() V70() V71() V72() Element of ExtREAL
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
K6( the carrier of B) is non empty set
bool the carrier of B is non empty Element of K6(K6( the carrier of B))
K6(K6( the carrier of B)) is non empty set
PFuncs (DYADIC,(bool the carrier of B)) is non empty functional set
S is Element of K6( the carrier of B)
L is Element of K6( the carrier of B)
r is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of B)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of B))) (B,S,L)
F is Element of the carrier of B
(B,S,L,r,F) is V67() Element of K6(ExtREAL)
x is non empty V67() Element of K6(ExtREAL)
sup x is ext-real Element of ExtREAL
O2 is set
T is ext-real Element of ExtREAL
A is ext-real Element of ExtREAL
[.T,A.] is set
r0 is ext-real Element of ExtREAL
r1 is ext-real set
P is ext-real Element of ExtREAL
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
(T,A,B,S) is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
K7( the carrier of T, the carrier of R^1) is non empty V73() V74() V75() set
K6(K7( the carrier of T, the carrier of R^1)) is non empty set
(T,A,B,S) is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
K7(DOM,(bool the carrier of T)) is non empty set
K6(K7(DOM,(bool the carrier of T))) is non empty set
L is V11() real ext-real Element of DOM
(DOM,T,(T,A,B,S),L) is Element of K6( the carrier of T)
r is Element of the carrier of T
(T,A,B,S) . r is V11() real ext-real Element of REAL
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
F is ext-real Element of ExtREAL
x is V11() real ext-real Element of REAL
(T,A,B,S) . x is set
x is non empty V67() Element of K6(ExtREAL)
sup x is ext-real Element of ExtREAL
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
F is non empty V67() Element of K6(ExtREAL)
O2 is set
P is ext-real Element of ExtREAL
sup F is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
r0 is ext-real Element of ExtREAL
r1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic n is non empty V66() V67() V68() Element of K6(REAL)
r0 is ext-real Element of ExtREAL
r1 is V11() real ext-real Element of REAL
(T,A,B,S) . r1 is set
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
(T,A,B,S) is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
K7(DOM,(bool the carrier of T)) is non empty set
K6(K7(DOM,(bool the carrier of T))) is non empty set
(T,A,B,S) is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
K7( the carrier of T, the carrier of R^1) is non empty V73() V74() V75() set
K6(K7( the carrier of T, the carrier of R^1)) is non empty set
L is V11() real ext-real Element of REAL
(T,A,B,S) . L is set
r is Element of the carrier of T
(T,A,B,S) . r is V11() real ext-real Element of REAL
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
F is non empty V67() Element of K6(ExtREAL)
x is ext-real Element of ExtREAL
O2 is ext-real set
(L) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
P is V11() real ext-real Element of REAL
(P) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (P) is non empty V66() V67() V68() Element of K6(REAL)
(DYADIC,(bool the carrier of T),S,(P)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(DYADIC,(bool the carrier of T),S,(P)) . L is set
(T,A,B,S) . P is set
(DYADIC,(bool the carrier of T),S,(P)) . P is set
r1 is Relation-like dyadic (P) -defined bool the carrier of T -valued Function-like V33( dyadic (P), bool the carrier of T) (T,A,B,(P))
n is V11() real ext-real Element of dyadic (P)
((dyadic (P)),T,r1,n) is Element of K6( the carrier of T)
Cl ((dyadic (P)),T,r1,n) is Element of K6( the carrier of T)
D is V11() real ext-real Element of dyadic (P)
((dyadic (P)),T,r1,D) is Element of K6( the carrier of T)
P is V11() real ext-real Element of REAL
(P) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
(L) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic (P) is non empty V66() V67() V68() Element of K6(REAL)
dyadic (L) is non empty V66() V67() V68() Element of K6(REAL)
(DYADIC,(bool the carrier of T),S,(L)) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of T))
(T,A,B,S) . P is set
(DYADIC,(bool the carrier of T),S,(L)) . P is set
(DYADIC,(bool the carrier of T),S,(L)) . L is set
r1 is Relation-like dyadic (L) -defined bool the carrier of T -valued Function-like V33( dyadic (L), bool the carrier of T) (T,A,B,(L))
D is V11() real ext-real Element of dyadic (L)
((dyadic (L)),T,r1,D) is Element of K6( the carrier of T)
Cl ((dyadic (L)),T,r1,D) is Element of K6( the carrier of T)
n is V11() real ext-real Element of dyadic (L)
((dyadic (L)),T,r1,n) is Element of K6( the carrier of T)
(L) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
P is V11() real ext-real Element of REAL
(P) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
sup F is ext-real Element of ExtREAL
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
x is non empty V67() Element of K6(ExtREAL)
sup x is ext-real Element of ExtREAL
F is ext-real Element of ExtREAL
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
(T,A,B,S,r) is V67() Element of K6(ExtREAL)
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
S is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
(T,A,B,S) is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
K7( the carrier of T, the carrier of R^1) is non empty V73() V74() V75() set
K6(K7( the carrier of T, the carrier of R^1)) is non empty set
(T,A,B,S) is Relation-like DOM -defined bool the carrier of T -valued Function-like V33( DOM , bool the carrier of T) Element of K6(K7(DOM,(bool the carrier of T)))
K7(DOM,(bool the carrier of T)) is non empty set
K6(K7(DOM,(bool the carrier of T))) is non empty set
L is V11() real ext-real Element of DOM
(DOM,T,(T,A,B,S),L) is Element of K6( the carrier of T)
r is Element of the carrier of T
(T,A,B,S) . r is V11() real ext-real Element of REAL
A is non empty TopSpace-like normal TopStruct
the carrier of A is non empty set
K6( the carrier of A) is non empty set
bool the carrier of A is non empty Element of K6(K6( the carrier of A))
K6(K6( the carrier of A)) is non empty set
PFuncs (DYADIC,(bool the carrier of A)) is non empty functional set
B is closed Element of K6( the carrier of A)
S is closed Element of K6( the carrier of A)
L is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of A)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of A))) (A,B,S)
(A,B,S,L) is Relation-like the carrier of A -defined the carrier of R^1 -valued Function-like V33( the carrier of A, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of A, the carrier of R^1))
K7( the carrier of A, the carrier of R^1) is non empty V73() V74() V75() set
K6(K7( the carrier of A, the carrier of R^1)) is non empty set
r is Element of the carrier of A
(A,B,S,L) . r is V11() real ext-real Element of REAL
(A,B,S,L,r) is V67() Element of K6(ExtREAL)
(DYADIC,(bool the carrier of A),L,0) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of A))
[#] A is non empty non proper closed Element of K6( the carrier of A)
(DYADIC,(bool the carrier of A),L,0) . 1 is set
([#] A) \ ((DYADIC,(bool the carrier of A),L,0) . 1) is Element of K6( the carrier of A)
(A,B,S,L) is Relation-like DOM -defined bool the carrier of A -valued Function-like V33( DOM , bool the carrier of A) Element of K6(K7(DOM,(bool the carrier of A)))
K7(DOM,(bool the carrier of A)) is non empty set
K6(K7(DOM,(bool the carrier of A))) is non empty set
(A,B,S,L) . 1 is set
F is V11() real ext-real Element of REAL
(A,B,S,L) . F is set
(A,B,S,L,r) is V67() Element of K6(ExtREAL)
F is ext-real Element of ExtREAL
x is V11() real ext-real Element of REAL
O2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic O2 is non empty V66() V67() V68() Element of K6(REAL)
(A,B,S,L) is Relation-like DOM -defined bool the carrier of A -valued Function-like V33( DOM , bool the carrier of A) Element of K6(K7(DOM,(bool the carrier of A)))
K7(DOM,(bool the carrier of A)) is non empty set
K6(K7(DOM,(bool the carrier of A))) is non empty set
(A,B,S,L) . x is set
(DYADIC,(bool the carrier of A),L,O2) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of A))
(DYADIC,(bool the carrier of A),L,O2) . x is set
r1 is Relation-like dyadic O2 -defined bool the carrier of A -valued Function-like V33( dyadic O2, bool the carrier of A) (A,B,S,O2)
r1 . 0 is set
r1 is Relation-like dyadic O2 -defined bool the carrier of A -valued Function-like V33( dyadic O2, bool the carrier of A) (A,B,S,O2)
P is V11() real ext-real Element of dyadic O2
((dyadic O2),A,r1,P) is Element of K6( the carrier of A)
Cl ((dyadic O2),A,r1,P) is Element of K6( the carrier of A)
r0 is V11() real ext-real Element of dyadic O2
((dyadic O2),A,r1,r0) is Element of K6( the carrier of A)
r1 . 0 is set
r1 . x is set
(DYADIC,(bool the carrier of A),L,0) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of A))
(DYADIC,(bool the carrier of A),L,0) . 0 is set
(A,B,S,L) is Relation-like DOM -defined bool the carrier of A -valued Function-like V33( DOM , bool the carrier of A) Element of K6(K7(DOM,(bool the carrier of A)))
K7(DOM,(bool the carrier of A)) is non empty set
K6(K7(DOM,(bool the carrier of A))) is non empty set
(A,B,S,L) . 0 is set
F is set
x is V11() real ext-real Element of REAL
O2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic O2 is non empty V66() V67() V68() Element of K6(REAL)
F is non empty V67() Element of K6(ExtREAL)
sup F is ext-real Element of ExtREAL
T is ext-real Element of ExtREAL
(DYADIC,(bool the carrier of A),L,0) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of A))
[#] A is non empty non proper closed Element of K6( the carrier of A)
(DYADIC,(bool the carrier of A),L,0) . 1 is set
([#] A) \ ((DYADIC,(bool the carrier of A),L,0) . 1) is Element of K6( the carrier of A)
(A,B,S,L) is Relation-like DOM -defined bool the carrier of A -valued Function-like V33( DOM , bool the carrier of A) Element of K6(K7(DOM,(bool the carrier of A)))
K7(DOM,(bool the carrier of A)) is non empty set
K6(K7(DOM,(bool the carrier of A))) is non empty set
(A,B,S,L) . 1 is set
x is V11() real ext-real Element of REAL
(A,B,S,L) . x is set
x is non empty V67() Element of K6(ExtREAL)
sup x is ext-real Element of ExtREAL
(A,B,S,L,r) is V67() Element of K6(ExtREAL)
(A,B,S,L,r) is V67() Element of K6(ExtREAL)
r is Element of the carrier of A
K6( the carrier of R^1) is non empty set
(A,B,S,L) . r is V11() real ext-real Element of REAL
F is V66() V67() V68() Element of K6( the carrier of R^1)
the topology of R^1 is non empty Element of K6(K6( the carrier of R^1))
K6(K6( the carrier of R^1)) is non empty set
Family_open_set RealSpace is Element of K6(K6( the carrier of RealSpace))
K6( the carrier of RealSpace) is non empty set
K6(K6( the carrier of RealSpace)) is non empty set
O2 is V66() V67() V68() Element of K6(REAL)
x is V11() real ext-real Element of the carrier of RealSpace
P is V11() real ext-real Element of REAL
Ball (x,P) is V66() V67() V68() Element of K6( the carrier of RealSpace)
r0 is V11() real ext-real set
r1 is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
r1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V61() V66() V67() V68() V69() V70() V71() Element of NAT
dyadic n is non empty V66() V67() V68() Element of K6(REAL)
(DYADIC,(bool the carrier of A),L,n) is Relation-like Function-like Element of PFuncs (DYADIC,(bool the carrier of A))
(A,B,S,L) is Relation-like DOM -defined bool the carrier of A -valued Function-like V33( DOM , bool the carrier of A) Element of K6(K7(DOM,(bool the carrier of A)))
K7(DOM,(bool the carrier of A)) is non empty set
K6(K7(DOM,(bool the carrier of A))) is non empty set
(A,B,S,L) . r1 is set
(DYADIC,(bool the carrier of A),L,n) . r1 is set
r1 is Element of the carrier of A
(A,B,S,L) . r1 is V11() real ext-real Element of REAL
D is Relation-like dyadic n -defined bool the carrier of A -valued Function-like V33( dyadic n, bool the carrier of A) (A,B,S,n)
r1 is V11() real ext-real Element of dyadic n
((dyadic n),A,D,r1) is Element of K6( the carrier of A)
H is Element of K6( the carrier of A)
(A,B,S,L) .: H is V66() V67() V68() set
r1 is set
dom (A,B,S,L) is set
r2 is set
(A,B,S,L) . r2 is V11() real ext-real Element of REAL
B is V11() real ext-real Element of the carrier of RealSpace
x is V11() real ext-real Element of REAL
C is V11() real ext-real Element of REAL
x - C is V11() real ext-real Element of REAL
- (x - C) is V11() real ext-real Element of REAL
r3 is Element of the carrier of A
(A,B,S,L) . r3 is V11() real ext-real Element of REAL
P - 0 is V11() real ext-real Element of REAL
C - x is V11() real ext-real Element of REAL
abs (x - C) is V11() real ext-real Element of REAL
dist (x,B) is V11() real ext-real Element of REAL
- (- (x - C)) is V11() real ext-real Element of REAL
- P is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
r1 is V11() real ext-real Element of REAL
r2 is V11() real ext-real Element of REAL
r2 - r1 is V11() real ext-real Element of REAL
(A,B,S,L) . r1 is set
[#] A is non empty non proper closed Element of K6( the carrier of A)
B is Element of K6( the carrier of A)
Cl B is Element of K6( the carrier of A)
([#] A) \ (Cl B) is Element of K6( the carrier of A)
r3 is V11() real ext-real Element of REAL
Cl (Cl B) is Element of K6( the carrier of A)
C is Element of K6( the carrier of A)
(A,B,S,L) . r3 is set
A is Element of K6( the carrier of A)
A /\ C is Element of K6( the carrier of A)
H is Element of K6( the carrier of A)
(A,B,S,L) .: H is V66() V67() V68() set
r4 is set
r4 is V11() real ext-real Element of the carrier of RealSpace
dom (A,B,S,L) is set
x1 is set
(A,B,S,L) . x1 is V11() real ext-real Element of REAL
x1 is Element of the carrier of A
y is V11() real ext-real Element of REAL
y is V11() real ext-real Element of the carrier of RealSpace
p is V11() real ext-real Element of REAL
q is V11() real ext-real Element of REAL
p - q is V11() real ext-real Element of REAL
- (p - q) is V11() real ext-real Element of REAL
- (- (p - q)) is V11() real ext-real Element of REAL
(A,B,S,L) . x1 is V11() real ext-real Element of REAL
q - p is V11() real ext-real Element of REAL
- P is V11() real ext-real Element of REAL
dist (r4,y) is V11() real ext-real Element of REAL
abs (p - q) is V11() real ext-real Element of REAL
Ball (r4,P) is V66() V67() V68() Element of K6( the carrier of RealSpace)
r4 is V11() real ext-real Element of REAL
(A,B,S,L) . r4 is set
r4 is V11() real ext-real Element of DOM
(DOM,A,(A,B,S,L),r4) is Element of K6( the carrier of A)
x is Element of K6( the carrier of A)
(A,B,S,L) .: x is V66() V67() V68() set
r is Element of the carrier of A
(A,B,S,L) . r is V11() real ext-real Element of REAL
F is Element of the carrier of A
(A,B,S,L) . F is V11() real ext-real Element of REAL
x is Element of the carrier of A
(A,B,S,L) . x is V11() real ext-real Element of REAL
O2 is Element of the carrier of A
(A,B,S,L) . O2 is V11() real ext-real Element of REAL
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
K7( the carrier of T, the carrier of R^1) is non empty V73() V74() V75() set
K6(K7( the carrier of T, the carrier of R^1)) is non empty set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
bool the carrier of T is non empty Element of K6(K6( the carrier of T))
K6(K6( the carrier of T)) is non empty set
PFuncs (DYADIC,(bool the carrier of T)) is non empty functional set
the Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B) is Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)
(T,A,B, the Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)) is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
L is Element of the carrier of T
(T,A,B, the Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)) . L is V11() real ext-real Element of REAL
r is Element of the carrier of T
(T,A,B, the Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)) . r is V11() real ext-real Element of REAL
F is Element of the carrier of T
(T,A,B, the Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)) . F is V11() real ext-real Element of REAL
x is Element of the carrier of T
(T,A,B, the Relation-like NAT -defined PFuncs (DYADIC,(bool the carrier of T)) -valued Function-like V33( NAT , PFuncs (DYADIC,(bool the carrier of T))) (T,A,B)) . x is V11() real ext-real Element of REAL
T is non empty TopSpace-like normal TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
K7( the carrier of T, the carrier of R^1) is non empty V73() V74() V75() set
K6(K7( the carrier of T, the carrier of R^1)) is non empty set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
r is V11() real ext-real Element of the carrier of R^1
F is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
F is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like V33( the carrier of T, the carrier of R^1) V73() V74() V75() Element of K6(K7( the carrier of T, the carrier of R^1))
dom F is set
K6( the carrier of R^1) is non empty set
P is V66() V67() V68() Element of K6( the carrier of R^1)
K447( the carrier of T, the carrier of R^1,F,P) is Element of K6( the carrier of T)
O2 is Element of K6( the carrier of T)
[#] T is non empty non proper closed Element of K6( the carrier of T)
x is Element of K6( the carrier of T)
([#] T) \ x is Element of K6( the carrier of T)
r0 is set
F . r0 is V11() real ext-real Element of REAL
r1 is set
F . r1 is V11() real ext-real Element of REAL
r0 is set
F . r0 is V11() real ext-real Element of REAL
r1 is set
F . r1 is V11() real ext-real Element of REAL
x is Element of the carrier of T
F . x is V11() real ext-real Element of REAL
T is non empty TopSpace-like T_0 T_1 T_2 V123() normal T_3 T_4 V159() compact TopStruct
the carrier of T is non empty set
K6( the carrier of T) is non empty set
A is closed Element of K6( the carrier of T)
B is closed Element of K6( the carrier of T)
K7( the carrier of T, the carrier of R^1) is non empty V73() V74() V75() set
K6(K7( the carrier of T, the carrier of R^1)) is non empty set