:: ALI2 semantic presentation

REAL is non empty non finite V110() V111() V112() V116() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V110() V111() V112() V113() V114() V115() V116() Element of K10(REAL)

K10(REAL) is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal V110() V111() V112() V113() V114() V115() V116() set

K10(omega) is non empty set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

K11(1,1) is non empty set

K10(K11(1,1)) is non empty set

K11(K11(1,1),1) is non empty set

K10(K11(K11(1,1),1)) is non empty set

K11(K11(1,1),REAL) is non empty set

K10(K11(K11(1,1),REAL)) is non empty set

K11(REAL,REAL) is non empty set

K11(K11(REAL,REAL),REAL) is non empty set

K10(K11(K11(REAL,REAL),REAL)) is non empty set

2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

K11(2,2) is non empty set

K11(K11(2,2),REAL) is non empty set

K10(K11(K11(2,2),REAL)) is non empty set

COMPLEX is non empty non finite V110() V116() set

RAT is non empty non finite V110() V111() V112() V113() V116() set

INT is non empty non finite V110() V111() V112() V113() V114() V116() set

K11(COMPLEX,COMPLEX) is non empty set

K10(K11(COMPLEX,COMPLEX)) is non empty set

K11(K11(COMPLEX,COMPLEX),COMPLEX) is non empty set

K10(K11(K11(COMPLEX,COMPLEX),COMPLEX)) is non empty set

K10(K11(REAL,REAL)) is non empty set

K11(RAT,RAT) is non empty set

K10(K11(RAT,RAT)) is non empty set

K11(K11(RAT,RAT),RAT) is non empty set

K10(K11(K11(RAT,RAT),RAT)) is non empty set

K11(INT,INT) is non empty set

K10(K11(INT,INT)) is non empty set

K11(K11(INT,INT),INT) is non empty set

K10(K11(K11(INT,INT),INT)) is non empty set

K11(NAT,NAT) is non empty set

K11(K11(NAT,NAT),NAT) is non empty set

K10(K11(K11(NAT,NAT),NAT)) is non empty set

K10(NAT) is non empty set

{} is set

the empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V41() V42() V110() V111() V112() V113() V114() V115() V116() set is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V41() V42() V110() V111() V112() V113() V114() V115() V116() set

0 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

K11(NAT,REAL) is non empty set

K10(K11(NAT,REAL)) is non empty set

M is non empty Reflexive discerning V100() triangle Discerning MetrStruct

the carrier of M is non empty set

K11( the carrier of M, the carrier of M) is non empty set

K10(K11( the carrier of M, the carrier of M)) is non empty set

M is non empty Reflexive discerning V100() triangle Discerning MetrStruct

the carrier of M is non empty set

K11( the carrier of M, the carrier of M) is non empty set

K10(K11( the carrier of M, the carrier of M)) is non empty set

the Element of the carrier of M is Element of the carrier of M

the carrier of M --> the Element of the carrier of M is non empty V7() V10( the carrier of M) V11( the carrier of M) V12() V14() V17( the carrier of M) V21( the carrier of M, the carrier of M) Element of K10(K11( the carrier of M, the carrier of M))

x0 is non empty V12() V17( the carrier of M) V21( the carrier of M, the carrier of M) Element of K10(K11( the carrier of M, the carrier of M))

1 / 2 is ext-real non negative V41() V42() Element of REAL

a is Element of the carrier of M

x0 . a is Element of the carrier of M

L is Element of the carrier of M

x0 . L is Element of the carrier of M

dist ((x0 . a),(x0 . L)) is ext-real V41() V42() Element of REAL

dist (a,L) is ext-real V41() V42() Element of REAL

(1 / 2) * (dist (a,L)) is ext-real V41() V42() Element of REAL

M is non empty Reflexive discerning V100() triangle Discerning MetrStruct

the carrier of M is non empty set

K11( the carrier of M, the carrier of M) is non empty set

K10(K11( the carrier of M, the carrier of M)) is non empty set

TopSpaceMetr M is non empty strict TopSpace-like TopStruct

f is non empty V12() V17( the carrier of M) V21( the carrier of M, the carrier of M) (M) Element of K10(K11( the carrier of M, the carrier of M))

the Element of the carrier of M is Element of the carrier of M

f . the Element of the carrier of M is Element of the carrier of M

dist ( the Element of the carrier of M,(f . the Element of the carrier of M)) is ext-real V41() V42() Element of REAL

L is ext-real V41() V42() Element of REAL

the carrier of (TopSpaceMetr M) is non empty set

K10( the carrier of (TopSpaceMetr M)) is non empty set

K10(K10( the carrier of (TopSpaceMetr M))) is non empty set

c is Element of K10(K10( the carrier of (TopSpaceMetr M)))

0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

L to_power (0 + 1) is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power (0 + 1)) is ext-real V41() V42() Element of REAL

x is Element of K10( the carrier of (TopSpaceMetr M))

Family_open_set M is Element of K10(K10( the carrier of M))

K10( the carrier of M) is non empty set

K10(K10( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

x ` is Element of K10( the carrier of (TopSpaceMetr M))

the carrier of (TopSpaceMetr M) \ x is set

r is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

L to_power r is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r) is ext-real V41() V42() Element of REAL

{ b

c is Element of K10( the carrier of M)

s9 is Element of the carrier of M

f . s9 is Element of the carrier of M

dist (s9,(f . s9)) is ext-real V41() V42() Element of REAL

(dist (s9,(f . s9))) - ((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r)) is ext-real V41() V42() Element of REAL

((dist (s9,(f . s9))) - ((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r))) / 2 is ext-real V41() V42() Element of REAL

s is ext-real V41() V42() Element of REAL

Ball (s9,s) is Element of K10( the carrier of M)

n is set

B is Element of the carrier of M

dist (s9,B) is ext-real V41() V42() Element of REAL

2 * s is ext-real V41() V42() Element of REAL

2 * (dist (s9,B)) is ext-real V41() V42() Element of REAL

f . B is Element of the carrier of M

dist (B,(f . B)) is ext-real V41() V42() Element of REAL

(dist (B,(f . B))) + (2 * s) is ext-real V41() V42() Element of REAL

(dist (B,(f . B))) + (2 * (dist (s9,B))) is ext-real V41() V42() Element of REAL

dist (s9,(f . B)) is ext-real V41() V42() Element of REAL

(dist (s9,B)) + (dist (B,(f . B))) is ext-real V41() V42() Element of REAL

dist ((f . B),(f . s9)) is ext-real V41() V42() Element of REAL

(dist (s9,(f . B))) + (dist ((f . B),(f . s9))) is ext-real V41() V42() Element of REAL

((dist (s9,B)) + (dist (B,(f . B)))) + (dist ((f . B),(f . s9))) is ext-real V41() V42() Element of REAL

dist (B,s9) is ext-real V41() V42() Element of REAL

L * (dist (B,s9)) is ext-real V41() V42() Element of REAL

(dist ((f . B),(f . s9))) + (dist (B,s9)) is ext-real V41() V42() Element of REAL

(dist (B,s9)) + (dist (B,s9)) is ext-real V41() V42() Element of REAL

(dist (B,s9)) + (dist ((f . B),(f . s9))) is ext-real V41() V42() Element of REAL

(dist (B,(f . B))) + ((dist (B,s9)) + (dist ((f . B),(f . s9)))) is ext-real V41() V42() Element of REAL

2 * (dist (B,s9)) is ext-real V41() V42() Element of REAL

(dist (B,(f . B))) + (2 * (dist (B,s9))) is ext-real V41() V42() Element of REAL

(dist (B,(f . B))) + (dist (s9,B)) is ext-real V41() V42() Element of REAL

((dist (B,(f . B))) + (dist (s9,B))) + (dist ((f . B),(f . s9))) is ext-real V41() V42() Element of REAL

(dist (s9,(f . s9))) - (2 * s) is ext-real V41() V42() Element of REAL

c

f . c

dist (c

Family_open_set M is Element of K10(K10( the carrier of M))

K10( the carrier of M) is non empty set

K10(K10( the carrier of M)) is non empty set

TopStruct(# the carrier of M,(Family_open_set M) #) is strict TopStruct

{ b

{ b

x is set

meet x is set

c is set

r is set

s9 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

L to_power s9 is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power s9) is ext-real V41() V42() Element of REAL

{ b

s is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

L to_power s is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power s) is ext-real V41() V42() Element of REAL

{ b

n is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

B is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

L to_power B is ext-real V41() V42() Element of REAL

L to_power n is ext-real V41() V42() Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

B is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

L to_power B is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power B) is ext-real V41() V42() Element of REAL

L to_power n is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power n) is ext-real V41() V42() Element of REAL

n is set

B is Element of the carrier of M

f . B is Element of the carrier of M

dist (B,(f . B)) is ext-real V41() V42() Element of REAL

n is set

B is Element of the carrier of M

f . B is Element of the carrier of M

dist (B,(f . B)) is ext-real V41() V42() Element of REAL

c is set

r is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

L to_power r is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r) is ext-real V41() V42() Element of REAL

{ b

r + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

L to_power (r + 1) is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power (r + 1)) is ext-real V41() V42() Element of REAL

{ b

the Element of { b

L * ((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power r)) is ext-real V41() V42() Element of REAL

L * (L to_power r) is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L * (L to_power r)) is ext-real V41() V42() Element of REAL

L to_power 1 is ext-real V41() V42() Element of REAL

(L to_power r) * (L to_power 1) is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * ((L to_power r) * (L to_power 1)) is ext-real V41() V42() Element of REAL

s is Element of the carrier of M

f . s is Element of the carrier of M

dist (s,(f . s)) is ext-real V41() V42() Element of REAL

f . (f . s) is Element of the carrier of M

dist ((f . s),(f . (f . s))) is ext-real V41() V42() Element of REAL

L * (dist (s,(f . s))) is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * 1 is ext-real V41() V42() Element of REAL

L to_power 0 is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power 0) is ext-real V41() V42() Element of REAL

{ b

meet c is Element of K10( the carrier of (TopSpaceMetr M))

x is Element of the carrier of (TopSpaceMetr M)

c is Element of the carrier of M

f . c is Element of the carrier of M

dist (c,(f . c)) is ext-real V41() V42() Element of REAL

NAT --> (dist (c,(f . c))) is non empty V7() V10( NAT ) V11( REAL ) V12() V14() V17( NAT ) V21( NAT , REAL ) convergent Element of K10(K11(NAT,REAL))

s9 is non empty V12() V17( NAT ) V21( NAT , REAL ) Element of K10(K11(NAT,REAL))

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) (#) s9 is non empty V12() V17( NAT ) V21( NAT , REAL ) Element of K10(K11(NAT,REAL))

lim s9 is ext-real V41() V42() Element of REAL

lim ((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) (#) s9) is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * 0 is ext-real V41() V42() Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

n + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V41() V42() V108() V109() V110() V111() V112() V113() V114() V115() Element of NAT

L to_power (n + 1) is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (L to_power (n + 1)) is ext-real V41() V42() Element of REAL

{ b

((dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) (#) s9) . n is ext-real V41() V42() Element of REAL

s9 . n is ext-real V41() V42() Element of REAL

(dist ( the Element of the carrier of M,(f . the Element of the carrier of M))) * (s9 . n) is ext-real V41() V42() Element of REAL

r is non empty V12() V17( NAT ) V21( NAT , REAL ) Element of K10(K11(NAT,REAL))

r . n is ext-real V41() V42() Element of REAL

c

f . c

dist (c

lim r is ext-real V41() V42() Element of REAL

r . 0 is ext-real V41() V42() Element of REAL

c is Element of the carrier of M

f . c is Element of the carrier of M

dist (c,(f . c)) is ext-real V41() V42() Element of REAL

c is Element of the carrier of M

f . c is Element of the carrier of M

dist (c,(f . c)) is ext-real V41() V42() Element of REAL

x is Element of the carrier of M

f . x is Element of the carrier of M

dist (x,c) is ext-real V41() V42() Element of REAL

L * (dist (x,c)) is ext-real V41() V42() Element of REAL