:: URYSOHN3 semantic presentation

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