:: TOPMETR semantic presentation

REAL is complex-membered ext-real-membered real-membered V105() V108() V109() V111() set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V105() V108() Element of bool REAL

bool REAL is non empty set

COMPLEX is complex-membered V105() set

omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V105() V108() set

bool omega is non empty set

I[01] is non empty strict TopSpace-like TopStruct

the carrier of I[01] is non empty set

1 is non empty natural V14() real ext-real positive complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V106() V108() 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 set

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

[:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is set

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

2 is non empty natural V14() real ext-real positive complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V106() V108() Element of NAT

[:2,2:] is non empty set

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

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

{} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V105() V108() V111() set

0 is empty natural V14() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V105() V108() V111() Element of NAT

RealSpace is non empty strict Reflexive discerning V122() triangle Discerning MetrStruct

real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V36([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]

MetrStruct(# REAL,real_dist #) is strict MetrStruct

TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct

the carrier of RealSpace is non empty set

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

bool the carrier of RealSpace is non empty set

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

TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr RealSpace) is non empty set

bool the carrier of (TopSpaceMetr RealSpace) is non empty set

[.0,1.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

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

x is TopStruct

the carrier of x is set

bool the carrier of x is non empty set

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

R is Element of bool (bool the carrier of T)

union R is set

e is Element of bool (bool the carrier of x)

union e is set

T is non empty TopSpace-like TopStruct

R is non empty TopSpace-like SubSpace of T

the carrier of R is non empty set

bool the carrier of R is non empty set

x is Element of the carrier of R

e is Element of the carrier of R

the carrier of T is non empty set

bool the carrier of T is non empty set

B is Element of the carrier of T

A is Element of the carrier of T

B2 is Element of bool the carrier of T

r is Element of bool the carrier of T

[#] R is non empty non proper open closed dense non boundary Element of bool the carrier of R

B2 /\ ([#] R) is Element of bool the carrier of R

r /\ ([#] R) is Element of bool the carrier of R

the topology of T is non empty Element of bool (bool the carrier of T)

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

d is Element of bool the carrier of R

the topology of R is non empty Element of bool (bool the carrier of R)

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

W9 is Element of bool the carrier of R

B2 /\ r is Element of bool the carrier of T

W9 /\ d is Element of bool the carrier of R

B2 /\ (r /\ ([#] R)) is Element of bool the carrier of R

(B2 /\ (r /\ ([#] R))) /\ ([#] R) is Element of bool the carrier of R

{} /\ ([#] R) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V108() Element of bool the carrier of R

T is TopSpace-like TopStruct

R is TopSpace-like SubSpace of T

the carrier of R is set

x is TopSpace-like SubSpace of T

the carrier of x is set

bool the carrier of R is non empty set

the topology of R is non empty Element of bool (bool the carrier of R)

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

bool the carrier of x is non empty set

the topology of x is non empty Element of bool (bool the carrier of x)

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

[#] R is non proper open closed dense Element of bool the carrier of R

e is Element of bool the carrier of R

the carrier of T is set

bool the carrier of T is non empty set

the topology of T is non empty Element of bool (bool the carrier of T)

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

B is Element of bool the carrier of T

B /\ ([#] R) is Element of bool the carrier of R

[#] x is non proper open closed dense Element of bool the carrier of x

B /\ ([#] x) is Element of bool the carrier of x

A is Element of bool the carrier of x

([#] x) /\ ([#] R) is Element of bool the carrier of R

B /\ (([#] x) /\ ([#] R)) is Element of bool the carrier of R

A /\ ([#] R) is Element of bool the carrier of R

B is Element of bool the carrier of x

B /\ ([#] R) is Element of bool the carrier of R

the carrier of T is set

bool the carrier of T is non empty set

the topology of T is non empty Element of bool (bool the carrier of T)

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

[#] x is non proper open closed dense Element of bool the carrier of x

A is Element of bool the carrier of T

A /\ ([#] x) is Element of bool the carrier of x

([#] x) /\ ([#] R) is Element of bool the carrier of R

A /\ (([#] x) /\ ([#] R)) is Element of bool the carrier of R

A /\ ([#] R) is Element of bool the carrier of R

[#] x is non proper open closed dense Element of bool the carrier of x

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

R is Element of bool the carrier of T

T | R is strict TopSpace-like SubSpace of T

x is Element of bool the carrier of T

R \/ x is Element of bool the carrier of T

T | (R \/ x) is strict TopSpace-like SubSpace of T

T | x is strict TopSpace-like SubSpace of T

[#] (T | R) is non proper open closed dense Element of bool the carrier of (T | R)

the carrier of (T | R) is set

bool the carrier of (T | R) is non empty set

[#] (T | (R \/ x)) is non proper open closed dense Element of bool the carrier of (T | (R \/ x))

the carrier of (T | (R \/ x)) is set

bool the carrier of (T | (R \/ x)) is non empty set

[#] (T | x) is non proper open closed dense Element of bool the carrier of (T | x)

the carrier of (T | x) is set

bool the carrier of (T | x) is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

R is Element of the carrier of T

x is non empty Element of bool the carrier of T

T | x is non empty strict TopSpace-like SubSpace of T

the carrier of (T | x) is non empty set

bool the carrier of (T | x) is non empty set

e is a_neighborhood of R

e /\ x is Element of bool the carrier of T

B is Element of the carrier of (T | x)

A is Element of bool the carrier of (T | x)

Int e is open Element of bool the carrier of T

B2 is Element of bool the carrier of T

B2 /\ x is Element of bool the carrier of T

r is Element of bool the carrier of (T | x)

[#] (T | x) is non empty non proper open closed dense non boundary Element of bool the carrier of (T | x)

B2 /\ ([#] (T | x)) is Element of bool the carrier of (T | x)

Int A is open Element of bool the carrier of (T | x)

T is TopSpace-like TopStruct

the carrier of T is set

R is TopSpace-like TopStruct

the carrier of R is set

[: the carrier of T, the carrier of R:] is set

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

bool the carrier of R is non empty set

x is Relation-like the carrier of T -defined the carrier of R -valued Function-like V36( the carrier of T, the carrier of R) Element of bool [: the carrier of T, the carrier of R:]

e is Element of bool the carrier of R

R | e is strict TopSpace-like SubSpace of R

the carrier of (R | e) is set

[: the carrier of T, the carrier of (R | e):] is set

bool [: the carrier of T, the carrier of (R | e):] is non empty set

[#] (R | e) is non proper open closed dense Element of bool the carrier of (R | e)

bool the carrier of (R | e) is non empty set

B is Relation-like the carrier of T -defined the carrier of (R | e) -valued Function-like V36( the carrier of T, the carrier of (R | e)) Element of bool [: the carrier of T, the carrier of (R | e):]

rng x is Element of bool the carrier of R

A is Element of bool the carrier of (R | e)

B " A is Element of bool the carrier of T

bool the carrier of T is non empty set

B2 is Element of bool the carrier of R

B2 /\ ([#] (R | e)) is Element of bool the carrier of (R | e)

B2 /\ e is Element of bool the carrier of R

x " (B2 /\ e) is Element of bool the carrier of T

x " B2 is Element of bool the carrier of T

x " e is Element of bool the carrier of T

(x " B2) /\ (x " e) is Element of bool the carrier of T

(rng x) /\ e is Element of bool the carrier of R

x " ((rng x) /\ e) is Element of bool the carrier of T

(x " B2) /\ (x " ((rng x) /\ e)) is Element of bool the carrier of T

x " (rng x) is Element of bool the carrier of T

(x " B2) /\ (x " (rng x)) is Element of bool the carrier of T

dom x is Element of bool the carrier of T

(x " B2) /\ (dom x) is Element of bool the carrier of T

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

R is non empty TopStruct

the carrier of R is non empty set

[: the carrier of T, the carrier of R:] is set

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

x is Element of bool the carrier of T

T | x is strict SubSpace of T

the carrier of (T | x) is set

[: the carrier of (T | x), the carrier of R:] is set

bool [: the carrier of (T | x), the carrier of R:] is non empty set

e is Relation-like the carrier of T -defined the carrier of R -valued Function-like V36( the carrier of T, the carrier of R) Element of bool [: the carrier of T, the carrier of R:]

e | x is Relation-like the carrier of T -defined the carrier of R -valued Element of bool [: the carrier of T, the carrier of R:]

B is Relation-like the carrier of (T | x) -defined the carrier of R -valued Function-like V36( the carrier of (T | x), the carrier of R) Element of bool [: the carrier of (T | x), the carrier of R:]

[#] R is non empty non proper dense Element of bool the carrier of R

bool the carrier of R is non empty set

A is Element of bool the carrier of R

B " A is Element of bool the carrier of (T | x)

bool the carrier of (T | x) is non empty set

[#] (T | x) is non proper dense Element of bool the carrier of (T | x)

e " A is Element of bool the carrier of T

([#] (T | x)) /\ (e " A) is Element of bool the carrier of T

T is Reflexive discerning V122() triangle MetrStruct

the carrier of T is set

the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

[: the carrier of T, the carrier of T:] is set

[:[: the carrier of T, the carrier of T:],REAL:] is set

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

MetrStruct(# the carrier of T, the distance of T #) is strict MetrStruct

the carrier of MetrStruct(# the carrier of T, the distance of T #) is set

R is Element of the carrier of MetrStruct(# the carrier of T, the distance of T #)

x is Element of the carrier of MetrStruct(# the carrier of T, the distance of T #)

e is Element of the carrier of MetrStruct(# the carrier of T, the distance of T #)

dist (R,e) is V14() real ext-real Element of REAL

the distance of MetrStruct(# the carrier of T, the distance of T #) is Relation-like [: the carrier of MetrStruct(# the carrier of T, the distance of T #), the carrier of MetrStruct(# the carrier of T, the distance of T #):] -defined REAL -valued Function-like V36([: the carrier of MetrStruct(# the carrier of T, the distance of T #), the carrier of MetrStruct(# the carrier of T, the distance of T #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of T, the distance of T #), the carrier of MetrStruct(# the carrier of T, the distance of T #):],REAL:]

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

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

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

the distance of MetrStruct(# the carrier of T, the distance of T #) . (R,e) is V14() real ext-real Element of REAL

[R,e] is set

{R,e} is non empty set

{R} is non empty set

{{R,e},{R}} is non empty set

the distance of MetrStruct(# the carrier of T, the distance of T #) . [R,e] is set

the distance of T . (R,e) is set

the distance of T . [R,e] is set

B is Element of the carrier of T

B2 is Element of the carrier of T

dist (B,B2) is V14() real ext-real Element of REAL

the distance of T . (B,B2) is V14() real ext-real Element of REAL

[B,B2] is set

{B,B2} is non empty set

{B} is non empty set

{{B,B2},{B}} is non empty set

the distance of T . [B,B2] is set

dist (R,x) is V14() real ext-real Element of REAL

the distance of MetrStruct(# the carrier of T, the distance of T #) . (R,x) is V14() real ext-real Element of REAL

[R,x] is set

{R,x} is non empty set

{{R,x},{R}} is non empty set

the distance of MetrStruct(# the carrier of T, the distance of T #) . [R,x] is set

the distance of T . (R,x) is set

the distance of T . [R,x] is set

A is Element of the carrier of T

dist (B,A) is V14() real ext-real Element of REAL

the distance of T . (B,A) is V14() real ext-real Element of REAL

[B,A] is set

{B,A} is non empty set

{{B,A},{B}} is non empty set

the distance of T . [B,A] is set

dist (x,R) is V14() real ext-real Element of REAL

the distance of MetrStruct(# the carrier of T, the distance of T #) . (x,R) is V14() real ext-real Element of REAL

[x,R] is set

{x,R} is non empty set

{x} is non empty set

{{x,R},{x}} is non empty set

the distance of MetrStruct(# the carrier of T, the distance of T #) . [x,R] is set

the distance of T . (x,R) is set

the distance of T . [x,R] is set

dist (A,B) is V14() real ext-real Element of REAL

the distance of T . (A,B) is V14() real ext-real Element of REAL

[A,B] is set

{A,B} is non empty set

{A} is non empty set

{{A,B},{A}} is non empty set

the distance of T . [A,B] is set

dist (x,e) is V14() real ext-real Element of REAL

the distance of MetrStruct(# the carrier of T, the distance of T #) . (x,e) is V14() real ext-real Element of REAL

[x,e] is set

{x,e} is non empty set

{{x,e},{x}} is non empty set

the distance of MetrStruct(# the carrier of T, the distance of T #) . [x,e] is set

the distance of T . (x,e) is set

the distance of T . [x,e] is set

dist (A,B2) is V14() real ext-real Element of REAL

the distance of T . (A,B2) is V14() real ext-real Element of REAL

[A,B2] is set

{A,B2} is non empty set

{{A,B2},{A}} is non empty set

the distance of T . [A,B2] is set

(dist (R,x)) + (dist (x,e)) is V14() real ext-real Element of REAL

T is Reflexive discerning V122() triangle MetrStruct

the carrier of T is set

the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

[: the carrier of T, the carrier of T:] is set

[:[: the carrier of T, the carrier of T:],REAL:] is set

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

MetrStruct(# the carrier of T, the distance of T #) is strict MetrStruct

R is Reflexive discerning V122() triangle MetrStruct

the carrier of R is set

the distance of R is Relation-like [: the carrier of R, the carrier of R:] -defined REAL -valued Function-like V36([: the carrier of R, the carrier of R:], REAL ) Element of bool [:[: the carrier of R, the carrier of R:],REAL:]

[: the carrier of R, the carrier of R:] is set

[:[: the carrier of R, the carrier of R:],REAL:] is set

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

x is Element of the carrier of R

e is Element of the carrier of R

the distance of R . (x,e) is V14() real ext-real Element of REAL

[x,e] is set

{x,e} is non empty set

{x} is non empty set

{{x,e},{x}} is non empty set

the distance of R . [x,e] is set

the distance of T . (x,e) is set

the distance of T . [x,e] is set

T is Reflexive discerning V122() triangle MetrStruct

the carrier of T is set

the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

[: the carrier of T, the carrier of T:] is set

[:[: the carrier of T, the carrier of T:],REAL:] is set

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

MetrStruct(# the carrier of T, the distance of T #) is strict MetrStruct

R is Reflexive discerning V122() triangle MetrStruct

the carrier of R is set

the distance of R is Relation-like [: the carrier of R, the carrier of R:] -defined REAL -valued Function-like V36([: the carrier of R, the carrier of R:], REAL ) Element of bool [:[: the carrier of R, the carrier of R:],REAL:]

[: the carrier of R, the carrier of R:] is set

[:[: the carrier of R, the carrier of R:],REAL:] is set

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

x is Element of the carrier of R

e is Element of the carrier of R

the distance of R . (x,e) is V14() real ext-real Element of REAL

[x,e] is set

{x,e} is non empty set

{x} is non empty set

{{x,e},{x}} is non empty set

the distance of R . [x,e] is set

the distance of T . (x,e) is set

the distance of T . [x,e] is set

T is non empty Reflexive discerning V122() triangle Discerning MetrStruct

the carrier of T is non empty set

the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

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

[:[: the carrier of T, the carrier of T:],REAL:] is set

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

MetrStruct(# the carrier of T, the distance of T #) is non empty strict MetrStruct

R is Reflexive discerning V122() triangle MetrStruct

the carrier of R is set

the distance of R is Relation-like [: the carrier of R, the carrier of R:] -defined REAL -valued Function-like V36([: the carrier of R, the carrier of R:], REAL ) Element of bool [:[: the carrier of R, the carrier of R:],REAL:]

[: the carrier of R, the carrier of R:] is set

[:[: the carrier of R, the carrier of R:],REAL:] is set

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

x is Element of the carrier of R

e is Element of the carrier of R

the distance of R . (x,e) is V14() real ext-real Element of REAL

[x,e] is set

{x,e} is non empty set

{x} is non empty set

{{x,e},{x}} is non empty set

the distance of R . [x,e] is set

the distance of T . (x,e) is set

the distance of T . [x,e] is set

T is non empty Reflexive discerning V122() triangle Discerning MetrStruct

the carrier of T is non empty set

R is non empty Reflexive discerning V122() triangle Discerning (T)

the carrier of R is non empty set

x is Element of the carrier of R

T is V14() real ext-real set

R is Reflexive discerning V122() triangle MetrStruct

the carrier of R is set

x is Reflexive discerning V122() triangle (R)

the carrier of x is set

e is Element of the carrier of R

Ball (e,T) is Element of bool the carrier of R

bool the carrier of R is non empty set

(Ball (e,T)) /\ the carrier of x is Element of bool the carrier of R

B is Element of the carrier of x

Ball (B,T) is Element of bool the carrier of x

bool the carrier of x is non empty set

A is set

B2 is Element of the carrier of x

dist (B,B2) is V14() real ext-real Element of REAL

the distance of x is Relation-like [: the carrier of x, the carrier of x:] -defined REAL -valued Function-like V36([: 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 set

[:[: the carrier of x, the carrier of x:],REAL:] is set

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

the distance of x . (B,B2) is V14() real ext-real Element of REAL

[B,B2] is set

{B,B2} is non empty set

{B} is non empty set

{{B,B2},{B}} is non empty set

the distance of x . [B,B2] is set

the distance of R is Relation-like [: the carrier of R, the carrier of R:] -defined REAL -valued Function-like V36([: the carrier of R, the carrier of R:], REAL ) Element of bool [:[: the carrier of R, the carrier of R:],REAL:]

[: the carrier of R, the carrier of R:] is set

[:[: the carrier of R, the carrier of R:],REAL:] is set

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

r is Element of the carrier of R

the distance of R . (e,r) is V14() real ext-real Element of REAL

[e,r] is set

{e,r} is non empty set

{e} is non empty set

{{e,r},{e}} is non empty set

the distance of R . [e,r] is set

dist (e,r) is V14() real ext-real Element of REAL

A is set

B2 is Element of the carrier of x

r is Element of the carrier of R

dist (e,r) is V14() real ext-real Element of REAL

the distance of R . (e,r) is V14() real ext-real Element of REAL

[e,r] is set

{e,r} is non empty set

{{e,r},{e}} is non empty set

the distance of R . [e,r] is set

the distance of x . (B,B2) is V14() real ext-real Element of REAL

[B,B2] is set

{B,B2} is non empty set

{{B,B2},{B}} is non empty set

the distance of x . [B,B2] is set

dist (B,B2) is V14() real ext-real Element of REAL

T is non empty Reflexive discerning V122() triangle Discerning MetrStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

R is non empty Element of bool the carrier of T

the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

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

[:[: the carrier of T, the carrier of T:],REAL:] is set

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

the distance of T || R is Relation-like Function-like set

[:R,R:] is non empty set

the distance of T | [:R,R:] is Relation-like set

dom ( the distance of T || R) is set

dom the distance of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

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

(dom the distance of T) /\ [:R,R:] is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] /\ [:R,R:] is set

the carrier of T /\ R is Element of bool the carrier of T

[:( the carrier of T /\ R),( the carrier of T /\ R):] is set

[:( the carrier of T /\ R),R:] is set

the distance of T | [:R,R:] is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

rng ( the distance of T || R) is set

x is non empty set

[:x,x:] is non empty set

[:[:x,x:],REAL:] is set

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

B is Relation-like [:x,x:] -defined REAL -valued Function-like V36([:x,x:], REAL ) Element of bool [:[:x,x:],REAL:]

MetrStruct(# x,B #) is non empty strict MetrStruct

the carrier of MetrStruct(# x,B #) is non empty set

B2 is Element of the carrier of MetrStruct(# x,B #)

r is Element of the carrier of MetrStruct(# x,B #)

dist (B2,r) is V14() real ext-real Element of REAL

the distance of MetrStruct(# x,B #) is Relation-like [: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):] -defined REAL -valued Function-like V36([: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):],REAL:]

[: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):] is non empty set

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

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

the distance of MetrStruct(# x,B #) . (B2,r) is V14() real ext-real Element of REAL

[B2,r] is set

{B2,r} is non empty set

{B2} is non empty set

{{B2,r},{B2}} is non empty set

the distance of MetrStruct(# x,B #) . [B2,r] is set

[B2,r] is Element of [: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):]

the distance of T . [B2,r] is set

the distance of T . (B2,r) is set

the distance of T . [B2,r] is set

B2 is Element of the carrier of MetrStruct(# x,B #)

r is Element of the carrier of MetrStruct(# x,B #)

W9 is Element of the carrier of MetrStruct(# x,B #)

dist (B2,W9) is V14() real ext-real Element of REAL

the distance of MetrStruct(# x,B #) . (B2,W9) is V14() real ext-real Element of REAL

[B2,W9] is set

{B2,W9} is non empty set

{B2} is non empty set

{{B2,W9},{B2}} is non empty set

the distance of MetrStruct(# x,B #) . [B2,W9] is set

the distance of T . (B2,W9) is set

the distance of T . [B2,W9] is set

d is Element of the carrier of T

H is Element of the carrier of T

dist (d,H) is V14() real ext-real Element of REAL

the distance of T . (d,H) is V14() real ext-real Element of REAL

[d,H] is set

{d,H} is non empty set

{d} is non empty set

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

the distance of T . [d,H] is set

dist (B2,r) is V14() real ext-real Element of REAL

the distance of MetrStruct(# x,B #) . (B2,r) is V14() real ext-real Element of REAL

[B2,r] is set

{B2,r} is non empty set

{{B2,r},{B2}} is non empty set

the distance of MetrStruct(# x,B #) . [B2,r] is set

the distance of T . (B2,r) is set

the distance of T . [B2,r] is set

H is Element of the carrier of T

dist (d,H) is V14() real ext-real Element of REAL

the distance of T . (d,H) is V14() real ext-real Element of REAL

[d,H] is set

{d,H} is non empty set

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

the distance of T . [d,H] is set

dist (r,W9) is V14() real ext-real Element of REAL

the distance of MetrStruct(# x,B #) . (r,W9) is V14() real ext-real Element of REAL

[r,W9] is set

{r,W9} is non empty set

{r} is non empty set

{{r,W9},{r}} is non empty set

the distance of MetrStruct(# x,B #) . [r,W9] is set

the distance of T . (r,W9) is set

the distance of T . [r,W9] is set

dist (H,H) is V14() real ext-real Element of REAL

the distance of T . (H,H) is V14() real ext-real Element of REAL

[H,H] is set

{H,H} is non empty set

{H} is non empty set

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

the distance of T . [H,H] is set

dist (H,d) is V14() real ext-real Element of REAL

the distance of T . (H,d) is V14() real ext-real Element of REAL

[H,d] is set

{H,d} is non empty set

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

the distance of T . [H,d] is set

dist (r,B2) is V14() real ext-real Element of REAL

the distance of MetrStruct(# x,B #) . (r,B2) is V14() real ext-real Element of REAL

[r,B2] is set

{r,B2} is non empty set

{{r,B2},{r}} is non empty set

the distance of MetrStruct(# x,B #) . [r,B2] is set

(dist (B2,r)) + (dist (r,W9)) is V14() real ext-real Element of REAL

B2 is Reflexive discerning V122() triangle MetrStruct

the carrier of B2 is set

the distance of B2 is Relation-like [: the carrier of B2, the carrier of B2:] -defined REAL -valued Function-like V36([: the carrier of B2, the carrier of B2:], REAL ) Element of bool [:[: the carrier of B2, the carrier of B2:],REAL:]

[: the carrier of B2, the carrier of B2:] is set

[:[: the carrier of B2, the carrier of B2:],REAL:] is set

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

r is Element of the carrier of B2

W9 is Element of the carrier of B2

the distance of B2 . (r,W9) is V14() real ext-real Element of REAL

[r,W9] is set

{r,W9} is non empty set

{r} is non empty set

{{r,W9},{r}} is non empty set

the distance of B2 . [r,W9] is set

dist (r,W9) is V14() real ext-real Element of REAL

the distance of T . (r,W9) is set

the distance of T . [r,W9] is set

r is strict Reflexive discerning V122() triangle (T)

the carrier of r is set

x is strict Reflexive discerning V122() triangle (T)

the carrier of x is set

e is strict Reflexive discerning V122() triangle (T)

the carrier of e is set

the distance of x is Relation-like [: the carrier of x, the carrier of x:] -defined REAL -valued Function-like V36([: 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 set

[:[: the carrier of x, the carrier of x:],REAL:] is set

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

B is Element of R

A is Element of R

the distance of x . (B,A) is set

[B,A] is set

{B,A} is non empty set

{B} is non empty set

{{B,A},{B}} is non empty set

the distance of x . [B,A] is set

the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

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

[:[: the carrier of T, the carrier of T:],REAL:] is set

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

the distance of T . (B,A) is V14() real ext-real Element of REAL

the distance of T . [B,A] is set

the distance of e is Relation-like [: the carrier of e, the carrier of e:] -defined REAL -valued Function-like V36([: the carrier of e, the carrier of e:], REAL ) Element of bool [:[: the carrier of e, the carrier of e:],REAL:]

[: the carrier of e, the carrier of e:] is set

[:[: the carrier of e, the carrier of e:],REAL:] is set

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

the distance of e . (B,A) is set

the distance of e . [B,A] is set

T is non empty Reflexive discerning V122() triangle Discerning MetrStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

R is non empty Element of bool the carrier of T

(T,R) is strict Reflexive discerning V122() triangle (T)

T is V14() real ext-real set

R is V14() real ext-real set

[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL

x is Element of bool the carrier of RealSpace

e is non empty Element of bool the carrier of RealSpace

(RealSpace,e) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

B is non empty Element of bool the carrier of RealSpace

(RealSpace,B) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

x is Element of bool the carrier of RealSpace

B is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

A is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

e is non empty Element of bool the carrier of RealSpace

(RealSpace,e) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

T is V14() real ext-real set

R is V14() real ext-real set

(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

the carrier of (T,R) is non empty set

[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL

x is non empty Element of bool the carrier of RealSpace

(RealSpace,x) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

the carrier of (RealSpace,x) is non empty set

T is MetrStruct

the carrier of T is set

bool the carrier of T is non empty set

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

x is V14() real ext-real set

T is Element of the carrier of RealSpace

e is V14() real ext-real set

R is Element of the carrier of RealSpace

dist (T,R) is V14() real ext-real Element of REAL

the distance of RealSpace is Relation-like [: the carrier of RealSpace, the carrier of RealSpace:] -defined REAL -valued Function-like V36([: the carrier of RealSpace, the carrier of RealSpace:], REAL ) Element of bool [:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:]

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

[:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:] is set

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

the distance of RealSpace . (T,R) is V14() real ext-real Element of REAL

[T,R] is set

{T,R} is non empty set

{T} is non empty set

{{T,R},{T}} is non empty set

the distance of RealSpace . [T,R] is set

x - e is V14() real ext-real set

abs (x - e) is V14() real ext-real Element of REAL

T is MetrStruct

the carrier of T is set

TopSpaceMetr T is strict TopSpace-like TopStruct

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

bool the carrier of T is non empty set

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

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

the carrier of (TopSpaceMetr T) is set

R is MetrStruct

TopSpaceMetr R is strict TopSpace-like TopStruct

the carrier of R is set

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

bool the carrier of R is non empty set

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

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

the topology of (TopSpaceMetr R) is non empty Element of bool (bool the carrier of (TopSpaceMetr R))

the carrier of (TopSpaceMetr R) is set

bool the carrier of (TopSpaceMetr R) is non empty set

bool (bool the carrier of (TopSpaceMetr R)) is non empty set

T is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr T is non empty strict TopSpace-like TopStruct

the carrier of T is non empty set

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

bool the carrier of T is non empty set

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

TopStruct(# the carrier of T,(Family_open_set T) #) is non empty strict TopStruct

R is non empty Reflexive discerning V122() triangle Discerning (T)

TopSpaceMetr R is non empty strict TopSpace-like TopStruct

the carrier of R is non empty set

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

bool the carrier of R is non empty set

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

TopStruct(# the carrier of R,(Family_open_set R) #) is non empty strict TopStruct

[#] (TopSpaceMetr R) is non empty non proper open closed dense non boundary Element of bool the carrier of (TopSpaceMetr R)

the carrier of (TopSpaceMetr R) is non empty set

bool the carrier of (TopSpaceMetr R) is non empty set

[#] (TopSpaceMetr T) is non empty non proper open closed dense non boundary Element of bool the carrier of (TopSpaceMetr T)

the carrier of (TopSpaceMetr T) is non empty set

bool the carrier of (TopSpaceMetr T) is non empty set

the topology of (TopSpaceMetr R) is non empty Element of bool (bool the carrier of (TopSpaceMetr R))

bool (bool the carrier of (TopSpaceMetr R)) is non empty set

the topology of (TopSpaceMetr T) is non empty Element of bool (bool the carrier of (TopSpaceMetr T))

bool (bool the carrier of (TopSpaceMetr T)) is non empty set

B is Element of bool the carrier of (TopSpaceMetr R)

{ (Ball (b

B2 is set

r is Element of the carrier of T

W9 is V14() real ext-real Element of REAL

Ball (r,W9) is Element of bool the carrier of T

(Ball (r,W9)) /\ the carrier of R is Element of bool the carrier of T

union { (Ball (b

B2 is Element of bool the carrier of T

r is Element of bool the carrier of (TopSpaceMetr T)

r /\ ([#] (TopSpaceMetr R)) is Element of bool the carrier of (TopSpaceMetr R)

d is set

H is Element of the carrier of R

W9 is Element of bool the carrier of R

W99 is V14() real ext-real Element of REAL

Ball (H,W99) is Element of bool the carrier of R

H is Element of the carrier of T

Ball (H,W99) is Element of bool the carrier of T

(Ball (H,W99)) /\ the carrier of R is Element of bool the carrier of T

W9 is Element of the carrier of T

d is set

H is Element of the carrier of T

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

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

(Ball (H,H)) /\ the carrier of R is Element of bool the carrier of T

W99 is V14() real ext-real Element of REAL

Ball (W9,W99) is Element of bool the carrier of T

W9 is set

d is set

H is Element of the carrier of T

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

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

(Ball (H,H)) /\ the carrier of R is Element of bool the carrier of T

B2 is Element of bool the carrier of (TopSpaceMetr T)

B2 /\ ([#] (TopSpaceMetr R)) is Element of bool the carrier of (TopSpaceMetr R)

A is Element of bool the carrier of R

W9 is Element of the carrier of R

d is Element of the carrier of T

r is Element of bool the carrier of T

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

Ball (d,H) is Element of bool the carrier of T

Ball (W9,H) is Element of bool the carrier of R

(Ball (d,H)) /\ the carrier of R is Element of bool the carrier of T

B2 /\ the carrier of R is Element of bool the carrier of (TopSpaceMetr T)

B2 /\ the carrier of (TopSpaceMetr R) is Element of bool the carrier of (TopSpaceMetr T)

T is V14() real ext-real set

R is triangle MetrStruct

the carrier of R is set

TopSpaceMetr R is strict TopSpace-like TopStruct

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

bool the carrier of R is non empty set

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

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

the carrier of (TopSpaceMetr R) is set

bool the carrier of (TopSpaceMetr R) is non empty set

x is Element of the carrier of R

Ball (x,T) is Element of bool the carrier of R

e is Element of bool the carrier of (TopSpaceMetr R)

T is non empty Reflexive discerning V122() triangle Discerning MetrStruct

TopSpaceMetr T is non empty strict TopSpace-like TopStruct

the carrier of T is non empty set

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

bool the carrier of T is non empty set

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

TopStruct(# the carrier of T,(Family_open_set T) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr T) is non empty set

bool the carrier of (TopSpaceMetr T) is non empty set

R is Element of bool the carrier of (TopSpaceMetr T)

the topology of (TopSpaceMetr T) is non empty Element of bool (bool the carrier of (TopSpaceMetr T))

bool (bool the carrier of (TopSpaceMetr T)) is non empty set

x is Element of bool the carrier of T

e is Element of the carrier of T

B is V14() real ext-real Element of REAL

Ball (e,B) is Element of bool the carrier of T

e is Element of the carrier of T

B is V14() real ext-real set

Ball (e,B) is Element of bool the carrier of T

A is V14() real ext-real Element of REAL

Ball (e,A) is Element of bool the carrier of T

x is Element of bool the carrier of T

the topology of (TopSpaceMetr T) is non empty Element of bool (bool the carrier of (TopSpaceMetr T))

bool (bool the carrier of (TopSpaceMetr T)) is non empty set

T is non empty Reflexive discerning V122() triangle Discerning MetrStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

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

TopSpaceMetr T is non empty strict TopSpace-like TopStruct

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

TopStruct(# the carrier of T,(Family_open_set T) #) is non empty strict TopStruct

x is Element of bool (bool the carrier of T)

the carrier of (TopSpaceMetr T) is non empty set

bool the carrier of (TopSpaceMetr T) is non empty set

bool (bool the carrier of (TopSpaceMetr T)) is non empty set

e is Element of bool (bool the carrier of (TopSpaceMetr T))

B is Element of bool the carrier of (TopSpaceMetr T)

A is Element of bool the carrier of T

B2 is Element of the carrier of T

r is V14() real ext-real Element of REAL

Ball (B2,r) is Element of bool the carrier of T

union x is set

union e is set

B is Element of bool (bool the carrier of (TopSpaceMetr T))

A is Element of bool (bool the carrier of T)

union B is set

union A is set

TopSpaceMetr T is non empty strict TopSpace-like TopStruct

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

TopStruct(# the carrier of T,(Family_open_set T) #) is non empty strict TopStruct

the carrier of (TopSpaceMetr T) is non empty set

bool the carrier of (TopSpaceMetr T) is non empty set

bool (bool the carrier of (TopSpaceMetr T)) is non empty set

x is Element of bool (bool the carrier of (TopSpaceMetr T))

{ (Ball (b

( b

B is set

A is Element of the carrier of T

B2 is V14() real ext-real Element of REAL

Ball (A,B2) is Element of bool the carrier of T

r is Element of bool the carrier of (TopSpaceMetr T)

B is Element of bool (bool the carrier of T)

union B is set

A is set

union x is set

B2 is Element of the carrier of T

r is set

W9 is Element of bool the carrier of (TopSpaceMetr T)

d is V14() real ext-real set

Ball (B2,d) is Element of bool the carrier of T

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

Ball (B2,H) is Element of bool the carrier of T

B2 is set

r is Element of the carrier of T

W9 is V14() real ext-real Element of REAL

Ball (r,W9) is Element of bool the carrier of T

d is Element of bool the carrier of (TopSpaceMetr T)

B2 is Element of bool (bool the carrier of T)

A is non empty Element of bool (bool the carrier of (TopSpaceMetr T))

r is set

W9 is Element of the carrier of T

d is V14() real ext-real Element of REAL

Ball (W9,d) is Element of bool the carrier of T

H is Element of bool the carrier of (TopSpaceMetr T)

H is Element of bool the carrier of (TopSpaceMetr T)

[:B2,A:] is set

bool [:B2,A:] is non empty set

r is Relation-like B2 -defined A -valued Function-like V36(B2,A) Element of bool [:B2,A:]

rng r is Element of bool A

bool A is non empty set

W9 is Element of bool (bool the carrier of (TopSpaceMetr T))

d is Element of bool (bool the carrier of (TopSpaceMetr T))

union d is set

union B2 is set

H is set

H is set

r . H is set

dom r is Element of bool B2

bool B2 is non empty set

dom r is Element of bool B2

bool B2 is non empty set

() is TopSpace-like TopStruct

the carrier of () is non empty set

T is V14() real ext-real set

R is V14() real ext-real set

(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct

the carrier of (T,R) is non empty set

Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))

bool the carrier of (T,R) is non empty set

bool (bool the carrier of (T,R)) is non empty set

TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct

T is V14() real ext-real set

R is V14() real ext-real set

(T,R) is non empty strict TopSpace-like SubSpace of ()

(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct

the carrier of (T,R) is non empty set

Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))

bool the carrier of (T,R) is non empty set

bool (bool the carrier of (T,R)) is non empty set

TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct

the carrier of (T,R) is non empty set

[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL

bool the carrier of () is non empty set

T is V14() real ext-real set

R is V14() real ext-real set

[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL

(T,R) is non empty strict TopSpace-like SubSpace of ()

(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct

the carrier of (T,R) is non empty set

Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))

bool the carrier of (T,R) is non empty set

bool (bool the carrier of (T,R)) is non empty set

TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct

x is Element of bool the carrier of ()

() | x is strict TopSpace-like SubSpace of ()

[#] (T,R) is non empty non proper open closed dense non boundary Element of bool the carrier of (T,R)

the carrier of (T,R) is non empty set

bool the carrier of (T,R) is non empty set

(0,1) is non empty strict TopSpace-like SubSpace of ()

(0,1) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

TopSpaceMetr (0,1) is non empty strict TopSpace-like TopStruct

the carrier of (0,1) is non empty set

Family_open_set (0,1) is Element of bool (bool the carrier of (0,1))

bool the carrier of (0,1) is non empty set

bool (bool the carrier of (0,1)) is non empty set

TopStruct(# the carrier of (0,1),(Family_open_set (0,1)) #) is non empty strict TopStruct

T is Element of bool the carrier of ()

x is Element of bool the carrier of (TopSpaceMetr RealSpace)

(TopSpaceMetr RealSpace) | x is strict TopSpace-like SubSpace of TopSpaceMetr RealSpace

T is V14() real ext-real set

R is V14() real ext-real set

x is V14() real ext-real set

T + x is V14() real ext-real set

(T + x) - x is V14() real ext-real set

R - x is V14() real ext-real set

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

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

T is Relation-like the carrier of () -defined the carrier of () -valued Function-like V36( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]

R is V14() real ext-real Element of REAL

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

e is Element of the carrier of ()

T . e is Element of the carrier of ()

B is a_neighborhood of T . e

Int B is open Element of bool the carrier of ()

B2 is Element of bool the carrier of ()

A is Element of the carrier of RealSpace

r is V14() real ext-real set

Ball (A,r) is Element of bool the carrier of RealSpace

[#] () is non empty non proper open closed dense non boundary Element of bool the carrier of ()

Int ([#] ()) is open Element of bool the carrier of ()

{x} is non empty complex-membered ext-real-membered real-membered set

dom T is Element of bool the carrier of ()

d is a_neighborhood of e

H is set

T . 0 is set

0 * 0 is V14() real ext-real Element of REAL

(0 * 0) + x is V14() real ext-real Element of REAL

H is set

T . H is set

W99 is V14() real ext-real Element of REAL

0 * W99 is V14() real ext-real Element of REAL

(0 * W99) + x is V14() real ext-real Element of REAL

T .: d is Element of bool the carrier of ()

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

0 * H is V14() real ext-real Element of REAL

(0 * H) + x is V14() real ext-real Element of REAL

abs R is V14() real ext-real Element of REAL

2 * (abs R) is V14() real ext-real Element of REAL

r / (2 * (abs R)) is V14() real ext-real Element of COMPLEX

W9 is Element of the carrier of RealSpace

Ball (W9,(r / (2 * (abs R)))) is Element of bool the carrier of RealSpace

H is Element of bool the carrier of ()

Int H is open Element of bool the carrier of ()

H is a_neighborhood of e

T .: H is Element of bool the carrier of ()

y is set

dom T is Element of bool the carrier of ()

x is set

T . x is set

x9 is Element of the carrier of RealSpace

y9 is V14() real ext-real Element of REAL

dist (W9,x9) is V14() real ext-real Element of REAL

the distance of RealSpace is Relation-like [: the carrier of RealSpace, the carrier of RealSpace:] -defined REAL -valued Function-like V36([: the carrier of RealSpace, the carrier of RealSpace:], REAL ) Element of bool [:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:]

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

[:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:] is set

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

the distance of RealSpace . (W9,x9) is V14() real ext-real Element of REAL

[W9,x9] is set

{W9,x9} is non empty set

{W9} is non empty set

{{W9,x9},{W9}} is non empty set

the distance of RealSpace . [W9,x9] is set

W99 is V14() real ext-real Element of REAL

x99 is V14() real ext-real Element of REAL

W99 - x99 is V14() real ext-real Element of REAL

abs (W99 - x99) is V14() real ext-real Element of REAL

(abs R) * (r / (2 * (abs R))) is V14() real ext-real Element of REAL

(abs R) * (abs (W99 - x99)) is V14() real ext-real Element of REAL

R * (W99 - x99) is V14() real ext-real Element of REAL

abs (R * (W99 - x99)) is V14() real ext-real Element of REAL

R * W99 is V14() real ext-real Element of REAL

(R * W99) + x is V14() real ext-real Element of REAL

R * x99 is V14() real ext-real Element of REAL

(R * x99) + x is V14() real ext-real Element of REAL

((R * W99) + x) - ((R * x99) + x) is V14() real ext-real Element of REAL

abs (((R * W99) + x) - ((R * x99) + x)) is V14() real ext-real Element of REAL

Y9 is V14() real ext-real Element of REAL

Y9 - ((R * x99) + x) is V14() real ext-real Element of REAL

abs (Y9 - ((R * x99) + x)) is V14() real ext-real Element of REAL

Y9 - y9 is V14() real ext-real Element of REAL

abs (Y9 - y9) is V14() real ext-real Element of REAL

r / 2 is V14() real ext-real Element of COMPLEX

(r / 2) + (r / 2) is V14() real ext-real Element of COMPLEX

yy is Element of the carrier of RealSpace

dist (A,yy) is V14() real ext-real Element of REAL

the distance of RealSpace . (A,yy) is V14() real ext-real Element of REAL

[A,yy] is set

{A,yy} is non empty set

{A} is non empty set

{{A,yy},{A}} is non empty set

the distance of RealSpace . [A,yy] is set

W9 is a_neighborhood of e

T .: W9 is Element of bool the carrier of ()

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

R is Element of bool the carrier of T

x is Element of bool the carrier of T

T | R is strict TopSpace-like SubSpace of T

T | x is strict TopSpace-like SubSpace of T

R \/ x is Element of bool the carrier of T

x is V14() real ext-real set

e is V14() real ext-real set

(x,e) is non empty strict TopSpace-like SubSpace of ()

(x,e) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

TopSpaceMetr (x,e) is non empty strict TopSpace-like TopStruct

the carrier of (x,e) is non empty set

Family_open_set (x,e) is Element of bool (bool the carrier of (x,e))

bool the carrier of (x,e) is non empty set

bool (bool the carrier of (x,e)) is non empty set

TopStruct(# the carrier of (x,e),(Family_open_set (x,e)) #) is non empty strict TopStruct

the carrier of (x,e) is non empty set

bool the carrier of (x,e) is non empty set

T is V14() real ext-real set

R is V14() real ext-real set

[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL

(T,R) is non empty strict TopSpace-like SubSpace of ()

(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct

the carrier of (T,R) is non empty set

Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))

bool the carrier of (T,R) is non empty set

bool (bool the carrier of (T,R)) is non empty set

TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct

B is Element of bool the carrier of (x,e)

(x,e) | B is strict TopSpace-like SubSpace of (x,e)

[.x,e.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL

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

() | B2 is non empty strict TopSpace-like SubSpace of ()

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

() | A is non empty strict TopSpace-like SubSpace of ()

() is non empty strict TopSpace-like SubSpace of ()

the carrier of () is non empty set

bool the carrier of () is non empty set

T is V14() real ext-real set

R is V14() real ext-real set

x is Element of bool the carrier of ()

[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL

(T,R) is non empty strict TopSpace-like SubSpace of ()

(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )

TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct

the carrier of (T,R) is non empty set

Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))

bool the carrier of (T,R) is non empty set

bool (bool the carrier of (T,R)) is non empty set

TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct

() | x is strict TopSpace-like SubSpace of ()

T is () 1-sorted

the carrier of T is set

T is set

T is () TopStruct

R is SubSpace of T

x is set

the carrier of R is set

the carrier of T is complex-membered ext-real-membered real-membered set