:: NORMSP_2 semantic presentation

REAL is non empty V34() set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is non empty set

COMPLEX is non empty V34() set

omega is non empty epsilon-transitive epsilon-connected ordinal set

bool omega is non empty set

bool NAT is non empty set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() real ext-real positive non negative Element of NAT

[:1,1:] is non empty set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is non empty set

bool [:[:1,1:],1:] is non empty set

[:[:1,1:],REAL:] is non empty set

bool [:[:1,1:],REAL:] is non empty set

[:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty set

bool [:[:REAL,REAL:],REAL:] is non empty set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V27() real ext-real positive non negative Element of NAT

[:2,2:] is non empty set

[:[:2,2:],REAL:] is non empty set

bool [:[:2,2:],REAL:] is non empty set

[:NAT,REAL:] is non empty set

bool [:NAT,REAL:] is non empty set

RAT is non empty V34() set

INT is non empty V34() set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real ext-real non positive non negative set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real ext-real non positive non negative Element of NAT

X is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

bool the carrier of X is non empty Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

bool (bool the carrier of X) is non empty set

[:NAT,(bool the carrier of X):] is non empty set

bool [:NAT,(bool the carrier of X):] is non empty set

Family_open_set X is Element of bool (bool the carrier of X)

Y is V10() V13( NAT ) V14( bool the carrier of X) Function-like V46( NAT , bool the carrier of X) Element of bool [:NAT,(bool the carrier of X):]

rng Y is Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

union (rng Y) is Element of bool the carrier of X

the Element of the carrier of X is Element of the carrier of X

Y . 0 is Element of bool the carrier of X

(Y . 0) ` is Element of bool the carrier of X

the carrier of X \ (Y . 0) is set

((Y . 0) `) ` is Element of bool the carrier of X

the carrier of X \ ((Y . 0) `) is set

the carrier of X \ ((Y . 0) `) is Element of bool the carrier of X

Ball ( the Element of the carrier of X,1) is Element of bool the carrier of X

f is set

ft is Element of the carrier of X

x is V27() real ext-real Element of REAL

Ball (ft,x) is Element of bool the carrier of X

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

min (x,(1 / 2)) is V27() real ext-real Element of REAL

xt is V27() real ext-real Element of REAL

1 / 1 is V27() real ext-real non negative Element of REAL

2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ 0) is V27() real ext-real Element of REAL

Ball (ft,xt) is Element of bool the carrier of X

(Ball (ft,xt)) /\ (Y . 0) is Element of bool the carrier of X

G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ G) is V27() real ext-real Element of REAL

Y . G is Element of bool the carrier of X

G + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ (G + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ (G + 1)) is V27() real ext-real Element of REAL

Y . (G + 1) is Element of bool the carrier of X

Gt is Element of the carrier of X

Ht is V27() real ext-real Element of REAL

Ball (Gt,Ht) is Element of bool the carrier of X

(Ball (Gt,Ht)) /\ (Y . G) is Element of bool the carrier of X

Ht / 2 is V27() real ext-real Element of REAL

Ball (Gt,(Ht / 2)) is Element of bool the carrier of X

G + 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ (G + 2) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ (G + 2)) is V27() real ext-real Element of REAL

(1 / (2 |^ (G + 1))) / 2 is V27() real ext-real Element of REAL

(G + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ ((G + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

(2 |^ (G + 1)) * 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

(Y . (G + 1)) ` is Element of bool the carrier of X

the carrier of X \ (Y . (G + 1)) is set

(Ball (Gt,(Ht / 2))) /\ ((Y . (G + 1)) `) is Element of bool the carrier of X

H is set

H is Element of the carrier of X

s is V27() real ext-real Element of REAL

Ball (H,s) is Element of bool the carrier of X

w is V27() real ext-real Element of REAL

Ball (H,w) is Element of bool the carrier of X

min (w,s) is V27() real ext-real Element of REAL

min ((min (w,s)),(1 / (2 |^ (G + 2)))) is V27() real ext-real Element of REAL

v is V27() real ext-real Element of REAL

Ball (H,v) is Element of bool the carrier of X

w1 is V27() real ext-real Element of REAL

v1 is Element of the carrier of X

Ball (v1,w1) is Element of bool the carrier of X

(Ball (v1,w1)) /\ (Y . (G + 1)) is Element of bool the carrier of X

H is V27() real ext-real Element of REAL

H is Element of the carrier of X

Ball (H,H) is Element of bool the carrier of X

(Ball (H,H)) /\ (Y . (G + 1)) is Element of bool the carrier of X

[:NAT, the carrier of X:] is non empty set

bool [:NAT, the carrier of X:] is non empty set

[: the carrier of X,REAL:] is non empty set

G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ G) is V27() real ext-real Element of REAL

Y . G is Element of bool the carrier of X

G + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ (G + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ (G + 1)) is V27() real ext-real Element of REAL

Y . (G + 1) is Element of bool the carrier of X

Gt is Element of [: the carrier of X,REAL:]

Gt `2 is V27() real ext-real Element of REAL

Gt `1 is Element of the carrier of X

Ball ((Gt `1),(Gt `2)) is Element of bool the carrier of X

(Ball ((Gt `1),(Gt `2))) /\ (Y . G) is Element of bool the carrier of X

(Gt `2) / 2 is V27() real ext-real Element of REAL

Ball ((Gt `1),((Gt `2) / 2)) is Element of bool the carrier of X

Ht is Element of the carrier of X

H is V27() real ext-real Element of REAL

Ball (Ht,H) is Element of bool the carrier of X

(Ball (Ht,H)) /\ (Y . (G + 1)) is Element of bool the carrier of X

[Ht,H] is Element of [: the carrier of X,REAL:]

{Ht,H} is non empty set

{Ht} is non empty set

{{Ht,H},{Ht}} is non empty set

[Ht,H] `2 is V27() real ext-real Element of REAL

[Ht,H] `1 is Element of the carrier of X

Ball (([Ht,H] `1),([Ht,H] `2)) is Element of bool the carrier of X

(Ball (([Ht,H] `1),([Ht,H] `2))) /\ (Y . (G + 1)) is Element of bool the carrier of X

[:NAT,[: the carrier of X,REAL:]:] is non empty set

bool [:NAT,[: the carrier of X,REAL:]:] is non empty set

[ft,xt] is Element of [: the carrier of X,REAL:]

{ft,xt} is non empty set

{ft} is non empty set

{{ft,xt},{ft}} is non empty set

G is V10() V13( NAT ) V14([: the carrier of X,REAL:]) Function-like V46( NAT ,[: the carrier of X,REAL:]) Element of bool [:NAT,[: the carrier of X,REAL:]:]

G . 0 is Element of [: the carrier of X,REAL:]

pr1 G is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

(pr1 G) . 0 is Element of the carrier of X

pr2 G is V10() V13( NAT ) V14( REAL ) Function-like V46( NAT , REAL ) Element of bool [:NAT,REAL:]

(pr2 G) . 0 is V27() real ext-real Element of REAL

(G . 0) `1 is Element of the carrier of X

(G . 0) `2 is V27() real ext-real Element of REAL

Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Gt + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . (Gt + 1) is Element of [: the carrier of X,REAL:]

(G . (Gt + 1)) `1 is Element of the carrier of X

(pr1 G) . (Gt + 1) is Element of the carrier of X

(G . (Gt + 1)) `2 is V27() real ext-real Element of REAL

(pr2 G) . (Gt + 1) is V27() real ext-real Element of REAL

G . Gt is Element of [: the carrier of X,REAL:]

(G . Gt) `1 is Element of the carrier of X

(pr1 G) . Gt is Element of the carrier of X

(G . Gt) `2 is V27() real ext-real Element of REAL

(pr2 G) . Gt is V27() real ext-real Element of REAL

2 |^ Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ Gt) is V27() real ext-real Element of REAL

Ball (((pr1 G) . Gt),((pr2 G) . Gt)) is Element of bool the carrier of X

Y . Gt is Element of bool the carrier of X

(Ball (((pr1 G) . Gt),((pr2 G) . Gt))) /\ (Y . Gt) is Element of bool the carrier of X

2 |^ (Gt + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ (Gt + 1)) is V27() real ext-real Element of REAL

Ball (((pr1 G) . (Gt + 1)),((pr2 G) . (Gt + 1))) is Element of bool the carrier of X

((pr2 G) . Gt) / 2 is V27() real ext-real Element of REAL

Ball (((pr1 G) . Gt),(((pr2 G) . Gt) / 2)) is Element of bool the carrier of X

Y . (Gt + 1) is Element of bool the carrier of X

(Ball (((pr1 G) . (Gt + 1)),((pr2 G) . (Gt + 1)))) /\ (Y . (Gt + 1)) is Element of bool the carrier of X

G is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

G . 0 is Element of the carrier of X

Gt is V10() V13( NAT ) V14( REAL ) Function-like V46( NAT , REAL ) Element of bool [:NAT,REAL:]

Gt . 0 is V27() real ext-real Element of REAL

G is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

G . 0 is Element of the carrier of X

Gt is V10() V13( NAT ) V14( REAL ) Function-like V46( NAT , REAL ) Element of bool [:NAT,REAL:]

Gt . 0 is V27() real ext-real Element of REAL

Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Gt . Ht is V27() real ext-real Element of REAL

2 |^ Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ Ht) is V27() real ext-real Element of REAL

Ht + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . (Ht + 1) is Element of the carrier of X

Gt . (Ht + 1) is V27() real ext-real Element of REAL

Ball ((G . (Ht + 1)),(Gt . (Ht + 1))) is Element of bool the carrier of X

G . Ht is Element of the carrier of X

(Gt . Ht) / 2 is V27() real ext-real Element of REAL

Ball ((G . Ht),((Gt . Ht) / 2)) is Element of bool the carrier of X

Ball ((G . Ht),(Gt . Ht)) is Element of bool the carrier of X

Y . Ht is Element of bool the carrier of X

(Ball ((G . Ht),(Gt . Ht))) /\ (Y . Ht) is Element of bool the carrier of X

Y . (Ht + 1) is Element of bool the carrier of X

(Ball ((G . (Ht + 1)),(Gt . (Ht + 1)))) /\ (Y . (Ht + 1)) is Element of bool the carrier of X

2 |^ (Ht + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ (Ht + 1)) is V27() real ext-real Element of REAL

(Ht + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . ((Ht + 1) + 1) is Element of the carrier of X

Gt . ((Ht + 1) + 1) is V27() real ext-real Element of REAL

Ball ((G . ((Ht + 1) + 1)),(Gt . ((Ht + 1) + 1))) is Element of bool the carrier of X

(Gt . (Ht + 1)) / 2 is V27() real ext-real Element of REAL

Ball ((G . (Ht + 1)),((Gt . (Ht + 1)) / 2)) is Element of bool the carrier of X

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V27() real ext-real positive non negative Element of NAT

G . (0 + 1) is Element of the carrier of X

Gt . (0 + 1) is V27() real ext-real Element of REAL

Ball ((G . (0 + 1)),(Gt . (0 + 1))) is Element of bool the carrier of X

(Gt . 0) / 2 is V27() real ext-real Element of REAL

Ball ((G . 0),((Gt . 0) / 2)) is Element of bool the carrier of X

Ball ((G . 0),(Gt . 0)) is Element of bool the carrier of X

(Ball ((G . 0),(Gt . 0))) /\ (Y . 0) is Element of bool the carrier of X

Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . Ht is Element of the carrier of X

2 |^ Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ Ht) is V27() real ext-real Element of REAL

H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Ht + H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . (Ht + H) is Element of the carrier of X

dist ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL

the distance of X is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

the distance of X . ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL

2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ H) is V27() real ext-real Element of REAL

1 - (1 / (2 |^ H)) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H))) is V27() real ext-real Element of REAL

(Ht + H) + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . ((Ht + H) + 1) is Element of the carrier of X

dist ((G . ((Ht + H) + 1)),(G . (Ht + H))) is V27() real ext-real Element of REAL

the distance of X . ((G . ((Ht + H) + 1)),(G . (Ht + H))) is V27() real ext-real Element of REAL

(dist ((G . ((Ht + H) + 1)),(G . (Ht + H)))) + (dist ((G . (Ht + H)),(G . Ht))) is V27() real ext-real Element of REAL

(dist ((G . ((Ht + H) + 1)),(G . (Ht + H)))) + ((1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL

Gt . ((Ht + H) + 1) is V27() real ext-real Element of REAL

dist ((G . ((Ht + H) + 1)),(G . ((Ht + H) + 1))) is V27() real ext-real Element of REAL

the distance of X . ((G . ((Ht + H) + 1)),(G . ((Ht + H) + 1))) is V27() real ext-real Element of REAL

Ball ((G . ((Ht + H) + 1)),(Gt . ((Ht + H) + 1))) is Element of bool the carrier of X

2 |^ (Ht + H) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ (Ht + H)) is V27() real ext-real Element of REAL

Gt . (Ht + H) is V27() real ext-real Element of REAL

(1 / (2 |^ (Ht + H))) / 2 is V27() real ext-real Element of REAL

(Gt . (Ht + H)) / 2 is V27() real ext-real Element of REAL

(2 |^ (Ht + H)) * 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / ((2 |^ (Ht + H)) * 2) is V27() real ext-real Element of REAL

2 |^ ((Ht + H) + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ ((Ht + H) + 1)) is V27() real ext-real Element of REAL

Ball ((G . (Ht + H)),((Gt . (Ht + H)) / 2)) is Element of bool the carrier of X

(1 / (2 |^ ((Ht + H) + 1))) + ((1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL

H + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Ht + (H + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ (Ht + (H + 1)) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ (H + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

(2 |^ Ht) * (2 |^ (H + 1)) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

(2 |^ (H + 1)) / 1 is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) / ((2 |^ (H + 1)) / 1) is V27() real ext-real Element of REAL

1 / (2 |^ (H + 1)) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 / (2 |^ (H + 1))) is V27() real ext-real Element of REAL

(1 / (2 |^ (H + 1))) - (1 / (2 |^ H)) is V27() real ext-real Element of REAL

1 + ((1 / (2 |^ (H + 1))) - (1 / (2 |^ H))) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 + ((1 / (2 |^ (H + 1))) - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL

(2 |^ H) * 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / ((2 |^ H) * 2) is V27() real ext-real Element of REAL

(1 / ((2 |^ H) * 2)) - (1 / (2 |^ H)) is V27() real ext-real Element of REAL

1 + ((1 / ((2 |^ H) * 2)) - (1 / (2 |^ H))) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 + ((1 / ((2 |^ H) * 2)) - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL

(1 / (2 |^ H)) / 2 is V27() real ext-real Element of REAL

((1 / (2 |^ H)) / 2) - (1 / (2 |^ H)) is V27() real ext-real Element of REAL

1 + (((1 / (2 |^ H)) / 2) - (1 / (2 |^ H))) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 + (((1 / (2 |^ H)) / 2) - (1 / (2 |^ H)))) is V27() real ext-real Element of REAL

1 - ((1 / (2 |^ H)) / 2) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 - ((1 / (2 |^ H)) / 2)) is V27() real ext-real Element of REAL

1 - (1 / ((2 |^ H) * 2)) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 - (1 / ((2 |^ H) * 2))) is V27() real ext-real Element of REAL

dist ((G . ((Ht + H) + 1)),(G . Ht)) is V27() real ext-real Element of REAL

the distance of X . ((G . ((Ht + H) + 1)),(G . Ht)) is V27() real ext-real Element of REAL

G . (Ht + (H + 1)) is Element of the carrier of X

dist ((G . (Ht + (H + 1))),(G . Ht)) is V27() real ext-real Element of REAL

the distance of X . ((G . (Ht + (H + 1))),(G . Ht)) is V27() real ext-real Element of REAL

1 - (1 / (2 |^ (H + 1))) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ (H + 1)))) is V27() real ext-real Element of REAL

Ht + 0 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . (Ht + 0) is Element of the carrier of X

dist ((G . (Ht + 0)),(G . Ht)) is V27() real ext-real Element of REAL

the distance of X . ((G . (Ht + 0)),(G . Ht)) is V27() real ext-real Element of REAL

1 - (1 / (2 |^ 0)) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ 0))) is V27() real ext-real Element of REAL

H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Ht + H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . (Ht + H) is Element of the carrier of X

dist ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL

the distance of X . ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL

2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ H) is V27() real ext-real Element of REAL

1 - (1 / (2 |^ H)) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H))) is V27() real ext-real Element of REAL

Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Ht + H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . (Ht + H) is Element of the carrier of X

G . Ht is Element of the carrier of X

dist ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL

the distance of X is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

the distance of X . ((G . (Ht + H)),(G . Ht)) is V27() real ext-real Element of REAL

2 |^ Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ Ht) is V27() real ext-real Element of REAL

2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ H) is V27() real ext-real Element of REAL

1 - (1 / (2 |^ H)) is V27() real ext-real Element of REAL

(1 / (2 |^ Ht)) * (1 - (1 / (2 |^ H))) is V27() real ext-real Element of REAL

1 - 0 is non empty V27() real ext-real positive non negative Element of REAL

(1 / (2 |^ Ht)) * 1 is V27() real ext-real Element of REAL

Ht is V27() real ext-real Element of REAL

H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ H) is V27() real ext-real Element of REAL

H + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

s is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

w is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

v is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real set

H + v is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

v1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

H + v1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

2 |^ H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / (2 |^ H) is V27() real ext-real Element of REAL

G . s is Element of the carrier of X

G . H is Element of the carrier of X

dist ((G . s),(G . H)) is V27() real ext-real Element of REAL

the distance of X . ((G . s),(G . H)) is V27() real ext-real Element of REAL

w1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real set

H + w1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

(2 |^ H) * 2 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

1 / ((2 |^ H) * 2) is V27() real ext-real Element of REAL

(1 / (2 |^ H)) / 2 is V27() real ext-real Element of REAL

zza is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

H + zza is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

(1 / (2 |^ H)) + (1 / (2 |^ H)) is V27() real ext-real Element of REAL

G . w is Element of the carrier of X

dist ((G . H),(G . w)) is V27() real ext-real Element of REAL

the distance of X . ((G . H),(G . w)) is V27() real ext-real Element of REAL

(dist ((G . s),(G . H))) + (dist ((G . H),(G . w))) is V27() real ext-real Element of REAL

dist ((G . s),(G . w)) is V27() real ext-real Element of REAL

the distance of X . ((G . s),(G . w)) is V27() real ext-real Element of REAL

Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Ht + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . Ht is Element of the carrier of X

Gt . Ht is V27() real ext-real Element of REAL

(Gt . Ht) / 2 is V27() real ext-real Element of REAL

Ball ((G . Ht),((Gt . Ht) / 2)) is Element of bool the carrier of X

H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

(Ht + 1) + H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . ((Ht + 1) + H) is Element of the carrier of X

Gt . ((Ht + 1) + H) is V27() real ext-real Element of REAL

Ball ((G . ((Ht + 1) + H)),(Gt . ((Ht + 1) + H))) is Element of bool the carrier of X

(Gt . ((Ht + 1) + H)) / 2 is V27() real ext-real Element of REAL

Ball ((G . ((Ht + 1) + H)),((Gt . ((Ht + 1) + H)) / 2)) is Element of bool the carrier of X

H + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

(Ht + 1) + (H + 1) is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . ((Ht + 1) + (H + 1)) is Element of the carrier of X

Gt . ((Ht + 1) + (H + 1)) is V27() real ext-real Element of REAL

Ball ((G . ((Ht + 1) + (H + 1))),(Gt . ((Ht + 1) + (H + 1)))) is Element of bool the carrier of X

((Ht + 1) + H) + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . (((Ht + 1) + H) + 1) is Element of the carrier of X

Gt . (((Ht + 1) + H) + 1) is V27() real ext-real Element of REAL

Ball ((G . (((Ht + 1) + H) + 1)),(Gt . (((Ht + 1) + H) + 1))) is Element of bool the carrier of X

(Ht + 1) + 0 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . ((Ht + 1) + 0) is Element of the carrier of X

Gt . ((Ht + 1) + 0) is V27() real ext-real Element of REAL

Ball ((G . ((Ht + 1) + 0)),(Gt . ((Ht + 1) + 0))) is Element of bool the carrier of X

Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Ht + 1 is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Gt . Ht is V27() real ext-real Element of REAL

(Gt . Ht) / 2 is V27() real ext-real Element of REAL

lim G is Element of the carrier of X

H is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

max (H,(Ht + 1)) is V27() real ext-real Element of REAL

s is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . s is Element of the carrier of X

dist ((G . s),(lim G)) is V27() real ext-real Element of REAL

the distance of X . ((G . s),(lim G)) is V27() real ext-real Element of REAL

w is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real set

(Ht + 1) + w is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

dist ((G . s),(G . s)) is V27() real ext-real Element of REAL

the distance of X . ((G . s),(G . s)) is V27() real ext-real Element of REAL

Gt . s is V27() real ext-real Element of REAL

Ball ((G . s),(Gt . s)) is Element of bool the carrier of X

v is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

(Ht + 1) + v is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

G . Ht is Element of the carrier of X

Ball ((G . Ht),((Gt . Ht) / 2)) is Element of bool the carrier of X

dist ((G . s),(G . Ht)) is V27() real ext-real Element of REAL

the distance of X . ((G . s),(G . Ht)) is V27() real ext-real Element of REAL

((Gt . Ht) / 2) + ((Gt . Ht) / 2) is V27() real ext-real Element of REAL

dist ((lim G),(G . s)) is V27() real ext-real Element of REAL

the distance of X . ((lim G),(G . s)) is V27() real ext-real Element of REAL

(dist ((lim G),(G . s))) + (dist ((G . s),(G . Ht))) is V27() real ext-real Element of REAL

dist ((lim G),(G . Ht)) is V27() real ext-real Element of REAL

the distance of X . ((lim G),(G . Ht)) is V27() real ext-real Element of REAL

Ball ((G . Ht),(Gt . Ht)) is Element of bool the carrier of X

Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Y . Ht is Element of bool the carrier of X

G . Ht is Element of the carrier of X

Gt . Ht is V27() real ext-real Element of REAL

Ball ((G . Ht),(Gt . Ht)) is Element of bool the carrier of X

(Ball ((G . Ht),(Gt . Ht))) /\ (Y . Ht) is Element of bool the carrier of X

Ht is set

dom Y is Element of bool NAT

H is set

Y . H is set

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

f is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

Y is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

f is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

ft is Element of the carrier of X

x is Element of the carrier of X

Y . (ft,x) is V27() real ext-real Element of REAL

ft - x is Element of the carrier of X

- x is Element of the carrier of X

ft + (- x) is Element of the carrier of X

the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

K239( the carrier of X, the addF of X,ft,(- x)) is Element of the carrier of X

||.(ft - x).|| is V27() real ext-real Element of REAL

f . (ft,x) is V27() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of MetrStruct(# the carrier of X,(X) #) is set

the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]

[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set

[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set

bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set

Y is Element of the carrier of X

(X) . (Y,Y) is V27() real ext-real Element of REAL

Y - Y is Element of the carrier of X

- Y is Element of the carrier of X

Y + (- Y) is Element of the carrier of X

the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

K239( the carrier of X, the addF of X,Y,(- Y)) is Element of the carrier of X

||.(Y - Y).|| is V27() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of MetrStruct(# the carrier of X,(X) #) is set

the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]

[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set

[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set

bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set

Y is Element of the carrier of X

f is Element of the carrier of X

(X) . (Y,f) is V27() real ext-real Element of REAL

Y - f is Element of the carrier of X

- f is Element of the carrier of X

Y + (- f) is Element of the carrier of X

the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

K239( the carrier of X, the addF of X,Y,(- f)) is Element of the carrier of X

||.(Y - f).|| is V27() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of MetrStruct(# the carrier of X,(X) #) is set

the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]

[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set

[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set

bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set

Y is Element of the carrier of X

f is Element of the carrier of X

(X) . (Y,f) is V27() real ext-real Element of REAL

Y - f is Element of the carrier of X

- f is Element of the carrier of X

Y + (- f) is Element of the carrier of X

the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

K239( the carrier of X, the addF of X,Y,(- f)) is Element of the carrier of X

||.(Y - f).|| is V27() real ext-real Element of REAL

f - Y is Element of the carrier of X

- Y is Element of the carrier of X

f + (- Y) is Element of the carrier of X

K239( the carrier of X, the addF of X,f,(- Y)) is Element of the carrier of X

||.(f - Y).|| is V27() real ext-real Element of REAL

(X) . (f,Y) is V27() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of MetrStruct(# the carrier of X,(X) #) is set

the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]

[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set

[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set

bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set

Y is Element of the carrier of X

ft is Element of the carrier of X

Y - ft is Element of the carrier of X

- ft is Element of the carrier of X

Y + (- ft) is Element of the carrier of X

the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

K239( the carrier of X, the addF of X,Y,(- ft)) is Element of the carrier of X

||.(Y - ft).|| is V27() real ext-real Element of REAL

f is Element of the carrier of X

Y - f is Element of the carrier of X

- f is Element of the carrier of X

Y + (- f) is Element of the carrier of X

K239( the carrier of X, the addF of X,Y,(- f)) is Element of the carrier of X

||.(Y - f).|| is V27() real ext-real Element of REAL

f - ft is Element of the carrier of X

f + (- ft) is Element of the carrier of X

K239( the carrier of X, the addF of X,f,(- ft)) is Element of the carrier of X

||.(f - ft).|| is V27() real ext-real Element of REAL

||.(Y - f).|| + ||.(f - ft).|| is V27() real ext-real Element of REAL

(X) . (f,ft) is V27() real ext-real Element of REAL

||.(Y - f).|| + ((X) . (f,ft)) is V27() real ext-real Element of REAL

(X) . (Y,f) is V27() real ext-real Element of REAL

((X) . (Y,f)) + ((X) . (f,ft)) is V27() real ext-real Element of REAL

(X) . (Y,ft) is V27() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of MetrStruct(# the carrier of X,(X) #) is set

the distance of MetrStruct(# the carrier of X,(X) #) is V10() V13([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):]) V14( REAL ) Function-like V46([: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:]

[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):] is set

[:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is set

bool [:[: the carrier of MetrStruct(# the carrier of X,(X) #), the carrier of MetrStruct(# the carrier of X,(X) #):],REAL:] is non empty set

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of (X) is non empty set

Y is Element of the carrier of (X)

f is V27() real ext-real set

Ball (Y,f) is Element of bool the carrier of (X)

bool the carrier of (X) is non empty set

{ b

xt is set

x is Element of the carrier of X

{ b

G is Element of the carrier of X

x - G is Element of the carrier of X

- G is Element of the carrier of X

x + (- G) is Element of the carrier of X

the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

K239( the carrier of X, the addF of X,x,(- G)) is Element of the carrier of X

||.(x - G).|| is V27() real ext-real Element of REAL

Gt is Element of the carrier of (X)

dist (Y,Gt) is V27() real ext-real Element of REAL

the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set

bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set

the distance of (X) . (Y,Gt) is V27() real ext-real Element of REAL

xt is set

G is Element of the carrier of (X)

dist (Y,G) is V27() real ext-real Element of REAL

the distance of (X) . (Y,G) is V27() real ext-real Element of REAL

Gt is Element of the carrier of X

x - Gt is Element of the carrier of X

- Gt is Element of the carrier of X

x + (- Gt) is Element of the carrier of X

K239( the carrier of X, the addF of X,x,(- Gt)) is Element of the carrier of X

||.(x - Gt).|| is V27() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of (X) is non empty set

Y is Element of the carrier of (X)

f is V27() real ext-real set

cl_Ball (Y,f) is Element of bool the carrier of (X)

bool the carrier of (X) is non empty set

{ b

xt is set

ft is Element of the carrier of X

{ b

G is Element of the carrier of X

ft - G is Element of the carrier of X

- G is Element of the carrier of X

ft + (- G) is Element of the carrier of X

the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

K239( the carrier of X, the addF of X,ft,(- G)) is Element of the carrier of X

||.(ft - G).|| is V27() real ext-real Element of REAL

Gt is Element of the carrier of (X)

dist (Y,Gt) is V27() real ext-real Element of REAL

the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set

bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set

the distance of (X) . (Y,Gt) is V27() real ext-real Element of REAL

xt is set

G is Element of the carrier of (X)

dist (Y,G) is V27() real ext-real Element of REAL

the distance of (X) . (Y,G) is V27() real ext-real Element of REAL

Gt is Element of the carrier of X

ft - Gt is Element of the carrier of X

- Gt is Element of the carrier of X

ft + (- Gt) is Element of the carrier of X

K239( the carrier of X, the addF of X,ft,(- Gt)) is Element of the carrier of X

||.(ft - Gt).|| is V27() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:NAT, the carrier of X:] is non empty set

bool [:NAT, the carrier of X:] is non empty set

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of (X) is non empty set

[:NAT, the carrier of (X):] is non empty set

bool [:NAT, the carrier of (X):] is non empty set

Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]

ft is Element of the carrier of X

x is Element of the carrier of (X)

xt is V27() real ext-real Element of REAL

G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Y . Ht is Element of the carrier of X

(Y . Ht) - ft is Element of the carrier of X

- ft is Element of the carrier of X

(Y . Ht) + (- ft) is Element of the carrier of X

the addF of X is V10() V13([: the carrier of X, the carrier of X:]) V14( the carrier of X) Function-like V46([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set

K239( the carrier of X, the addF of X,(Y . Ht),(- ft)) is Element of the carrier of X

||.((Y . Ht) - ft).|| is V27() real ext-real Element of REAL

f . Ht is Element of the carrier of (X)

dist ((f . Ht),x) is V27() real ext-real Element of REAL

the distance of (X) is V10() V13([: the carrier of (X), the carrier of (X):]) V14( REAL ) Function-like V46([: the carrier of (X), the carrier of (X):], REAL ) Element of bool [:[: the carrier of (X), the carrier of (X):],REAL:]

[: the carrier of (X), the carrier of (X):] is non empty set

[:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set

bool [:[: the carrier of (X), the carrier of (X):],REAL:] is non empty set

the distance of (X) . ((f . Ht),x) is V27() real ext-real Element of REAL

xt is V27() real ext-real Element of REAL

G is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Gt is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

Ht is epsilon-transitive epsilon-connected ordinal natural V27() real ext-real Element of NAT

f . Ht is Element of the carrier of (X)

dist ((f . Ht),x) is V27() real ext-real Element of REAL

the distance of (X) . ((f . Ht),x) is V27() real ext-real Element of REAL

Y . Ht is Element of the carrier of X

(Y . Ht) - ft is Element of the carrier of X

(Y . Ht) + (- ft) is Element of the carrier of X

K239( the carrier of X, the addF of X,(Y . Ht),(- ft)) is Element of the carrier of X

||.((Y . Ht) - ft).|| is V27() real ext-real Element of REAL

xt is V27() real ext-real Element of REAL

G is V27() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:NAT, the carrier of X:] is non empty set

bool [:NAT, the carrier of X:] is non empty set

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of (X) is non empty set

[:NAT, the carrier of (X):] is non empty set

bool [:NAT, the carrier of (X):] is non empty set

Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]

ft is Element of the carrier of X

x is Element of the carrier of (X)

ft is Element of the carrier of (X)

x is Element of the carrier of X

xt is V27() real ext-real Element of REAL

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:NAT, the carrier of X:] is non empty set

bool [:NAT, the carrier of X:] is non empty set

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

the carrier of (X) is non empty set

[:NAT, the carrier of (X):] is non empty set

bool [:NAT, the carrier of (X):] is non empty set

Y is V10() V13( NAT ) V14( the carrier of X) Function-like V46( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

lim Y is Element of the carrier of X

f is V10() V13( NAT ) V14( the carrier of (X)) Function-like V46( NAT , the carrier of (X)) Element of bool [:NAT, the carrier of (X):]

lim f is Element of the carrier of (X)

x is V27() real ext-real Element of REAL

ft is Element of the carrier of (X)

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct

the carrier of (X) is non empty set

Family_open_set (X) is Element of bool (bool the carrier of (X))

bool the carrier of (X) is non empty set

bool (bool the carrier of (X)) is non empty set

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

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

(X) is non empty TopSpace-like TopStruct

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct

the carrier of (X) is non empty set

Family_open_set (X) is Element of bool (bool the carrier of (X))

bool the carrier of (X) is non empty set

bool (bool the carrier of (X)) is non empty set

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

the carrier of (X) is non empty set

bool the carrier of (X) is non empty set

Y is Element of bool the carrier of (X)

f is Element of the carrier of (X)

ft is Element of the carrier of X

x is V27() real ext-real Element of REAL

{ b

xt is V27() real ext-real Element of REAL

Ball (f,xt) is Element of bool the carrier of (X)

G is Element of the carrier of X

{ b

the topology of (X) is Element of bool (bool the carrier of (X))

bool (bool the carrier of (X)) is non empty set

f is Element of the carrier of X

ft is Element of the carrier of (X)

x is V27() real ext-real Element of REAL

Ball (ft,x) is Element of bool the carrier of (X)

xt is V27() real ext-real Element of REAL

Ball (ft,xt) is Element of bool the carrier of (X)

{ b

G is Element of the carrier of X

{ b

f is Element of the carrier of X

ft is Element of the carrier of X

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

(X) is non empty TopSpace-like TopStruct

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct

the carrier of (X) is non empty set

Family_open_set (X) is Element of bool (bool the carrier of (X))

bool the carrier of (X) is non empty set

bool (bool the carrier of (X)) is non empty set

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

the carrier of (X) is non empty set

bool the carrier of (X) is non empty set

Y is Element of the carrier of X

f is V27() real ext-real Element of REAL

{ b

ft is Element of the carrier of (X)

Ball (ft,f) is Element of bool the carrier of (X)

x is Element of the carrier of X

{ b

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

(X) is non empty TopSpace-like TopStruct

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct

the carrier of (X) is non empty set

Family_open_set (X) is Element of bool (bool the carrier of (X))

bool the carrier of (X) is non empty set

bool (bool the carrier of (X)) is non empty set

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

the carrier of (X) is non empty set

bool the carrier of (X) is non empty set

Y is Element of the carrier of X

f is V27() real ext-real Element of REAL

{ b

ft is Element of the carrier of (X)

cl_Ball (ft,f) is Element of bool the carrier of (X)

x is Element of the carrier of X

{ b

X is non empty TopSpace-like T_2 TopStruct

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

(X) is non empty TopSpace-like TopStruct

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct

the carrier of (X) is non empty set

Family_open_set (X) is Element of bool (bool the carrier of (X))

bool the carrier of (X) is non empty set

bool (bool the carrier of (X)) is non empty set

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

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

(X) is non empty TopSpace-like TopStruct

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of X is non empty set

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct

the carrier of (X) is non empty set

Family_open_set (X) is Element of bool (bool the carrier of (X))

bool the carrier of (X) is non empty set

bool (bool the carrier of (X)) is non empty set

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

X is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:NAT, the carrier of X:] is non empty set

bool [:NAT, the carrier of X:] is non empty set

(X) is non empty TopSpace-like sequential TopStruct

(X) is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

(X) is V10() V13([: the carrier of X, the carrier of X:]) V14( REAL ) Function-like V46([: the carrier of X, the carrier of X:], REAL ) Element of bool [:[: the carrier of X, the carrier of X:],REAL:]

[: the carrier of X, the carrier of X:] is non empty set

[:[: the carrier of X, the carrier of X:],REAL:] is non empty set

bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set

MetrStruct(# the carrier of X,(X) #) is strict MetrStruct

TopSpaceMetr (X) is non empty strict TopSpace-like T_2 first-countable Frechet sequential TopStruct

the carrier of (X) is non empty set

Family_open_set (X) is Element of bool (bool the carrier of (X))

bool the carrier of (X) is non empty set

bool (bool the carrier of (X)) is non empty set

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

the carrier of (X) is non empty set

[:NAT, the carrier of (X):] is non empty set

bool [:NAT, the carrier of (X):] is non