:: HAUSDORF semantic presentation

NAT is V45() V46() V47() V48() V49() V50() V51() Element of K6(REAL)

REAL is non empty V45() V46() V47() V51() V52() set

K6(REAL) is non empty set

COMPLEX is non empty V45() V51() V52() set

RAT is non empty V45() V46() V47() V48() V51() V52() set

INT is non empty V45() V46() V47() V48() V49() V51() V52() set

omega is V45() V46() V47() V48() V49() V50() V51() set

K6(omega) is non empty set

K6(NAT) is non empty set

K7(COMPLEX,COMPLEX) is non empty V33() set

K6(K7(COMPLEX,COMPLEX)) is non empty set

K7(COMPLEX,REAL) is non empty V33() V34() V35() set

K6(K7(COMPLEX,REAL)) is non empty set

1 is non empty set

K7(1,1) is non empty set

K6(K7(1,1)) is non empty set

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

K6(K7(K7(1,1),1)) is non empty set

K7(K7(1,1),REAL) is non empty V33() V34() V35() set

K6(K7(K7(1,1),REAL)) is non empty set

K7(REAL,REAL) is non empty V33() V34() V35() set

K7(K7(REAL,REAL),REAL) is non empty V33() V34() V35() set

K6(K7(K7(REAL,REAL),REAL)) is non empty set

2 is non empty set

K7(2,2) is non empty set

K7(K7(2,2),REAL) is non empty V33() V34() V35() set

K6(K7(K7(2,2),REAL)) is non empty set

K391() is T_0 T_1 T_2 compact V147() TopStruct

the carrier of K391() is V45() V46() V47() set

RealSpace is strict V147() MetrStruct

R^1 is non empty strict TopSpace-like V147() TopStruct

the carrier of R^1 is non empty V45() V46() V47() set

K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty V33() set

K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set

K6(K7(REAL,REAL)) is non empty set

K7(RAT,RAT) is non empty V20( RAT ) V33() V34() V35() set

K6(K7(RAT,RAT)) is non empty set

K7(K7(RAT,RAT),RAT) is non empty V20( RAT ) V33() V34() V35() set

K6(K7(K7(RAT,RAT),RAT)) is non empty set

K7(INT,INT) is non empty V20( RAT ) V20( INT ) V33() V34() V35() set

K6(K7(INT,INT)) is non empty set

K7(K7(INT,INT),INT) is non empty V20( RAT ) V20( INT ) V33() V34() V35() set

K6(K7(K7(INT,INT),INT)) is non empty set

K7(NAT,NAT) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set

K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set

K6(K7(K7(NAT,NAT),NAT)) is non empty set

TOP-REAL 2 is V204() L16()

the carrier of (TOP-REAL 2) is set

K7( the carrier of (TOP-REAL 2),REAL) is V33() V34() V35() set

K6(K7( the carrier of (TOP-REAL 2),REAL)) is non empty set

K6( the carrier of (TOP-REAL 2)) is non empty set

{} is set

the empty V45() V46() V47() V48() V49() V50() V51() set is empty V45() V46() V47() V48() V49() V50() V51() set

0 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

K6( the carrier of R^1) is non empty set

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like TopStruct

n is V11() real ext-real set

P is V11() real ext-real set

max (n,P) is V11() real ext-real set

n is non empty Reflexive discerning V117() triangle MetrStruct

the carrier of n is non empty set

P is Element of the carrier of n

dist P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist P) . P is V11() real ext-real set

dist (P,P) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is Element of K6( the carrier of (TopSpaceMetr n))

Q is Element of the carrier of n

dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist Q) .: P is V45() V46() V47() Element of K6( the carrier of R^1)

dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))

(dist Q) . Q is V11() real ext-real set

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is Element of K6( the carrier of (TopSpaceMetr n))

Q is Element of the carrier of n

dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist Q) .: P is V45() V46() V47() Element of K6( the carrier of R^1)

R is V11() real ext-real set

dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))

P1 is set

(dist Q) . P1 is V11() real ext-real set

Q1 is Element of the carrier of n

dist (Q,Q1) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is set

(dist_min P) . Q is V11() real ext-real set

the carrier of n is non empty set

R is Element of the carrier of n

dist R is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

(dist R) .: P is V45() V46() V47() Element of K6( the carrier of R^1)

lower_bound ((dist R) .: P) is V11() real ext-real Element of REAL

[#] ((dist R) .: P) is V45() V46() V47() Element of K6(REAL)

lower_bound ([#] ((dist R) .: P)) is V11() real ext-real Element of REAL

Q1 is non empty V45() V46() V47() Element of K6(REAL)

lower_bound Q1 is V11() real ext-real Element of REAL

(dist_min P) . R is V11() real ext-real set

R1 is V11() real ext-real set

R1 is V11() real ext-real set

n is non empty Reflexive discerning V117() triangle MetrStruct

the carrier of n is non empty set

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is Element of the carrier of n

Q is Element of K6( the carrier of (TopSpaceMetr n))

Cl Q is Element of K6( the carrier of (TopSpaceMetr n))

R is V11() real ext-real set

Ball (P,R) is bounded Element of K6( the carrier of n)

K6( the carrier of n) is non empty set

P1 is set

Q1 is Element of the carrier of n

R1 is Element of the carrier of n

dist (P,R1) is V11() real ext-real Element of REAL

R is V11() real ext-real set

Ball (P,R) is bounded Element of K6( the carrier of n)

P1 is Element of the carrier of n

dist (P,P1) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is Element of the carrier of n

(dist_min P) . Q is V11() real ext-real set

dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

P1 is V11() real ext-real set

R is non empty V45() V46() V47() Element of K6(REAL)

Q1 is V11() real ext-real set

dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))

R1 is set

(dist Q) . R1 is V11() real ext-real set

y is Element of the carrier of n

dist (Q,y) is V11() real ext-real Element of REAL

lower_bound R is V11() real ext-real Element of REAL

lower_bound ((dist Q) .: P) is V11() real ext-real Element of REAL

[#] ((dist Q) .: P) is V45() V46() V47() Element of K6(REAL)

lower_bound ([#] ((dist Q) .: P)) is V11() real ext-real Element of REAL

P1 is V11() real ext-real set

dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))

Q1 is set

(dist Q) . Q1 is V11() real ext-real set

R1 is Element of the carrier of n

dist (Q,R1) is V11() real ext-real Element of REAL

P1 is V11() real ext-real set

Q1 is Element of the carrier of n

dist (Q,Q1) is V11() real ext-real Element of REAL

(dist Q) . Q1 is V11() real ext-real set

dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Cl P is Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is Element of the carrier of n

(dist_min P) . Q is V11() real ext-real set

R is V11() real ext-real set

R is V11() real ext-real set

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty closed Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is Element of the carrier of n

(dist_min P) . Q is V11() real ext-real set

Cl P is Element of K6( the carrier of (TopSpaceMetr n))

n is non empty V45() V46() V47() Element of K6( the carrier of R^1)

lower_bound n is V11() real ext-real Element of REAL

P is non empty V45() V46() V47() Element of K6(REAL)

lower_bound P is V11() real ext-real Element of REAL

[#] n is V45() V46() V47() Element of K6(REAL)

lower_bound ([#] n) is V11() real ext-real Element of REAL

n is non empty V45() V46() V47() Element of K6( the carrier of R^1)

upper_bound n is V11() real ext-real Element of REAL

P is non empty V45() V46() V47() Element of K6(REAL)

upper_bound P is V11() real ext-real Element of REAL

[#] n is V45() V46() V47() Element of K6(REAL)

upper_bound ([#] n) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is Element of the carrier of n

dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

R is V45() V46() V47() Element of K6(REAL)

P1 is ext-real set

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

R is Element of the carrier of n

Q is Element of the carrier of n

(dist_min P) . Q is V11() real ext-real set

dist (Q,R) is V11() real ext-real Element of REAL

dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))

(dist Q) . R is V11() real ext-real set

(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

lower_bound ((dist Q) .: P) is V11() real ext-real Element of REAL

P1 is non empty V45() V46() V47() Element of K6(REAL)

lower_bound P1 is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is V11() real ext-real set

R is Element of the carrier of n

(dist_min P) . R is V11() real ext-real set

dist R is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

(dist R) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

lower_bound ((dist R) .: P) is V11() real ext-real Element of REAL

P1 is non empty V45() V46() V47() Element of K6(REAL)

lower_bound P1 is V11() real ext-real Element of REAL

Q1 is V11() real ext-real set

dom (dist R) is Element of K6( the carrier of (TopSpaceMetr n))

R1 is set

(dist R) . R1 is V11() real ext-real set

y is Element of the carrier of n

dist (R,y) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is Element of the carrier of n

(dist_min P) . Q is V11() real ext-real set

R is Element of the carrier of n

dist (Q,R) is V11() real ext-real Element of REAL

(dist_min P) . R is V11() real ext-real set

(dist (Q,R)) + ((dist_min P) . R) is V11() real ext-real Element of REAL

P1 is Element of the carrier of n

dist (Q,P1) is V11() real ext-real Element of REAL

((dist_min P) . Q) - (dist (Q,R)) is V11() real ext-real Element of REAL

(dist (Q,P1)) - (dist (Q,R)) is V11() real ext-real Element of REAL

dist (R,P1) is V11() real ext-real Element of REAL

(dist (Q,R)) + (dist (R,P1)) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

K6( the carrier of n) is non empty set

P is Element of K6( the carrier of (TopSpaceMetr n))

(TopSpaceMetr n) | P is strict TopSpace-like SubSpace of TopSpaceMetr n

Q is non empty Element of K6( the carrier of n)

n | Q is non empty strict Reflexive discerning V117() triangle SubSpace of n

TopSpaceMetr (n | Q) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

R is TopSpace-like SubSpace of TopSpaceMetr n

the carrier of R is set

the carrier of (n | Q) is non empty set

[#] R is non proper closed Element of K6( the carrier of R)

K6( the carrier of R) is non empty set

n is non empty Reflexive discerning V117() triangle MetrStruct

the carrier of n is non empty set

K6( the carrier of n) is non empty set

P is Element of K6( the carrier of n)

Q is non empty Element of K6( the carrier of n)

n | Q is non empty strict Reflexive discerning V117() triangle SubSpace of n

the carrier of (n | Q) is non empty set

K6( the carrier of (n | Q)) is non empty set

R is Element of K6( the carrier of (n | Q))

P1 is V11() real ext-real Element of REAL

Q1 is Element of the carrier of n

R1 is Element of the carrier of n

dist (Q1,R1) is V11() real ext-real Element of REAL

the distance of (n | Q) is V16() V19(K7( the carrier of (n | Q), the carrier of (n | Q))) V20( REAL ) Function-like V30(K7( the carrier of (n | Q), the carrier of (n | Q)), REAL ) V33() V34() V35() Element of K6(K7(K7( the carrier of (n | Q), the carrier of (n | Q)),REAL))

K7( the carrier of (n | Q), the carrier of (n | Q)) is non empty set

K7(K7( the carrier of (n | Q), the carrier of (n | Q)),REAL) is non empty V33() V34() V35() set

K6(K7(K7( the carrier of (n | Q), the carrier of (n | Q)),REAL)) is non empty set

y is Element of the carrier of (n | Q)

z is Element of the carrier of (n | Q)

the distance of (n | Q) . (y,z) is V11() real ext-real Element of REAL

the distance of n is V16() V19(K7( the carrier of n, the carrier of n)) V20( REAL ) Function-like V30(K7( the carrier of n, the carrier of n), REAL ) V33() V34() V35() Element of K6(K7(K7( the carrier of n, the carrier of n),REAL))

K7( the carrier of n, the carrier of n) is non empty set

K7(K7( the carrier of n, the carrier of n),REAL) is non empty V33() V34() V35() set

K6(K7(K7( the carrier of n, the carrier of n),REAL)) is non empty set

the distance of n . (Q1,R1) is V11() real ext-real Element of REAL

dist (y,z) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

the carrier of n is non empty set

K6( the carrier of n) is non empty set

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is Element of K6( the carrier of n)

Q is Element of K6( the carrier of (TopSpaceMetr n))

(TopSpaceMetr n) | Q is strict TopSpace-like SubSpace of TopSpaceMetr n

the carrier of ((TopSpaceMetr n) | Q) is set

K6( the carrier of ((TopSpaceMetr n) | Q)) is non empty set

[#] ((TopSpaceMetr n) | Q) is non proper closed Element of K6( the carrier of ((TopSpaceMetr n) | Q))

P1 is Element of K6( the carrier of ((TopSpaceMetr n) | Q))

Q1 is non empty Element of K6( the carrier of n)

n | Q1 is non empty strict Reflexive discerning V117() triangle SubSpace of n

TopSpaceMetr (n | Q1) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

[#] (n | Q1) is non empty non proper Element of K6( the carrier of (n | Q1))

the carrier of (n | Q1) is non empty set

K6( the carrier of (n | Q1)) is non empty set

{} n is empty proper V45() V46() V47() V48() V49() V50() V51() bounded Element of K6( the carrier of n)

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is Element of the carrier of n

(dist_min P) . Q is V11() real ext-real set

R is set

P1 is Element of the carrier of n

dist (P1,Q) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

the carrier of n is non empty set

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

P is Element of the carrier of n

dist P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

the carrier of (TopSpaceMetr n) is non empty set

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty compact Element of K6( the carrier of (TopSpaceMetr n))

dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is Element of the carrier of n

dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() continuous Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

R is V45() V46() V47() Element of K6(REAL)

[#] ((dist Q) .: P) is V45() V46() V47() Element of K6(REAL)

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

R is Element of the carrier of n

Q is Element of the carrier of n

dist (Q,R) is V11() real ext-real Element of REAL

(dist_max P) . Q is V11() real ext-real set

dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() continuous Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

upper_bound ((dist Q) .: P) is V11() real ext-real Element of REAL

P1 is non empty V45() V46() V47() Element of K6(REAL)

upper_bound P1 is V11() real ext-real Element of REAL

dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))

(dist Q) . R is V11() real ext-real set

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is Element of the carrier of n

(dist_max P) . Q is V11() real ext-real set

R is set

P1 is Element of the carrier of n

dist (P1,Q) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

max_dist_max (P,Q) is V11() real ext-real Element of REAL

R is Element of the carrier of n

(dist_min P) . R is V11() real ext-real set

P1 is Element of the carrier of n

dist (P1,R) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

max_dist_max (P,Q) is V11() real ext-real Element of REAL

R is Element of the carrier of n

(dist_max P) . R is V11() real ext-real set

P1 is non empty compact Element of K6( the carrier of (TopSpaceMetr n))

dist_max P1 is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() continuous Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

(dist_max P1) .: Q is non empty V45() V46() V47() Element of K6( the carrier of R^1)

dom (dist_max P1) is Element of K6( the carrier of (TopSpaceMetr n))

(dist_max P1) . R is V11() real ext-real set

upper_bound ((dist_max P1) .: Q) is V11() real ext-real Element of REAL

max_dist_max (P1,Q) is V11() real ext-real Element of REAL

R1 is non empty V45() V46() V47() Element of K6(REAL)

upper_bound R1 is V11() real ext-real Element of REAL

[#] ((dist_max P1) .: Q) is V45() V46() V47() Element of K6(REAL)

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

(dist_max P) .: Q is non empty V45() V46() V47() Element of K6( the carrier of R^1)

R is V45() V46() V47() Element of K6(REAL)

the carrier of n is non empty set

K6( the carrier of n) is non empty set

max_dist_max (P,Q) is V11() real ext-real Element of REAL

Q1 is V11() real ext-real Element of REAL

R1 is ext-real set

dom (dist_max P) is Element of K6( the carrier of (TopSpaceMetr n))

y is set

(dist_max P) . y is V11() real ext-real set

P1 is non empty Element of K6( the carrier of n)

z is Element of the carrier of n

(dist_max P) . z is V11() real ext-real set

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

(dist_min P) .: Q is non empty V45() V46() V47() Element of K6( the carrier of R^1)

R is V45() V46() V47() Element of K6(REAL)

the carrier of n is non empty set

K6( the carrier of n) is non empty set

max_dist_max (P,Q) is V11() real ext-real Element of REAL

Q1 is V11() real ext-real Element of REAL

R1 is ext-real set

dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))

y is set

(dist_min P) . y is V11() real ext-real set

P1 is non empty Element of K6( the carrier of n)

z is Element of the carrier of n

(dist_min P) . z is V11() real ext-real set

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

Q is Element of the carrier of n

(dist_min P) . Q is V11() real ext-real set

(dist_max P) . Q is V11() real ext-real set

R is Element of the carrier of n

dist (R,Q) is V11() real ext-real Element of REAL

dist (Q,R) is V11() real ext-real Element of REAL

{0} is V45() V46() V47() V48() V49() V50() Element of K6(REAL)

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist_min P) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

Q is set

R is set

dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))

P1 is set

(dist_min P) . P1 is V11() real ext-real set

R is set

dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))

(dist_min P) . Q is V11() real ext-real set

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

max_dist_min (P,Q) is V11() real ext-real Element of REAL

the carrier of n is non empty set

R is Element of the carrier of n

P1 is Element of the carrier of n

dist (R,P1) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

max_dist_min (P,P) is V11() real ext-real Element of REAL

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist_min P) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

[#] ((dist_min P) .: P) is V45() V46() V47() Element of K6(REAL)

upper_bound ((dist_min P) .: P) is V11() real ext-real Element of REAL

upper_bound {0} is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

min_dist_max (P,Q) is V11() real ext-real Element of REAL

the carrier of n is non empty set

R is Element of the carrier of n

P1 is Element of the carrier of n

dist (R,P1) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

max_dist_min (Q,P) is V11() real ext-real Element of REAL

R is Element of the carrier of n

(dist_min Q) . R is V11() real ext-real set

(dist_min Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

upper_bound ((dist_min Q) .: P) is V11() real ext-real Element of REAL

Q1 is non empty V45() V46() V47() Element of K6(REAL)

upper_bound Q1 is V11() real ext-real Element of REAL

dom (dist_min Q) is Element of K6( the carrier of (TopSpaceMetr n))

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is Element of K6( the carrier of (TopSpaceMetr n))

Q is Element of K6( the carrier of (TopSpaceMetr n))

max_dist_min (P,Q) is V11() real ext-real Element of REAL

max_dist_min (Q,P) is V11() real ext-real Element of REAL

max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL

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

P1 is Element of K6( the carrier of (TopSpaceMetr n))

Q1 is Element of K6( the carrier of (TopSpaceMetr n))

max_dist_min (P1,Q1) is V11() real ext-real Element of REAL

max_dist_min (Q1,P1) is V11() real ext-real Element of REAL

max ((max_dist_min (P1,Q1)),(max_dist_min (Q1,P1))) is V11() real ext-real Element of REAL

max ((max_dist_min (Q1,P1)),(max_dist_min (P1,Q1))) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

the carrier of n is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(n,P,Q) is V11() real ext-real Element of REAL

max_dist_min (P,Q) is V11() real ext-real Element of REAL

max_dist_min (Q,P) is V11() real ext-real Element of REAL

max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL

R is Element of the carrier of n

(dist_min Q) . R is V11() real ext-real set

max ((max_dist_min (Q,P)),(max_dist_min (P,Q))) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

R is non empty Element of K6( the carrier of (TopSpaceMetr n))

max_dist_min (P,R) is V11() real ext-real Element of REAL

(n,P,Q) is V11() real ext-real Element of REAL

max_dist_min (P,Q) is V11() real ext-real Element of REAL

max_dist_min (Q,P) is V11() real ext-real Element of REAL

max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL

(n,Q,R) is V11() real ext-real Element of REAL

max_dist_min (Q,R) is V11() real ext-real Element of REAL

max_dist_min (R,Q) is V11() real ext-real Element of REAL

max ((max_dist_min (Q,R)),(max_dist_min (R,Q))) is V11() real ext-real Element of REAL

(n,P,Q) + (n,Q,R) is V11() real ext-real Element of REAL

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist_min P) .: R is non empty V45() V46() V47() Element of K6( the carrier of R^1)

P1 is non empty V45() V46() V47() Element of K6(REAL)

Q1 is V11() real ext-real set

dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))

R1 is set

(dist_min P) . R1 is V11() real ext-real set

the carrier of n is non empty set

y is Element of the carrier of n

(dist_min P) . y is V11() real ext-real set

(n,Q,P) is V11() real ext-real Element of REAL

max ((max_dist_min (Q,P)),(max_dist_min (P,Q))) is V11() real ext-real Element of REAL

((dist_min P) . y) - (n,Q,P) is V11() real ext-real Element of REAL

z is Element of the carrier of n

dist (y,z) is V11() real ext-real Element of REAL

(dist_min P) . z is V11() real ext-real set

(dist (y,z)) + ((dist_min P) . z) is V11() real ext-real Element of REAL

(dist (y,z)) + (n,Q,P) is V11() real ext-real Element of REAL

dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

(dist_min Q) . y is V11() real ext-real set

(n,Q,P) + ((dist_min Q) . y) is V11() real ext-real Element of REAL

(n,R,Q) is V11() real ext-real Element of REAL

max ((max_dist_min (R,Q)),(max_dist_min (Q,R))) is V11() real ext-real Element of REAL

(n,Q,P) + (n,Q,R) is V11() real ext-real Element of REAL

upper_bound P1 is V11() real ext-real Element of REAL

[#] ((dist_min P) .: R) is V45() V46() V47() Element of K6(REAL)

upper_bound ([#] ((dist_min P) .: R)) is V11() real ext-real Element of REAL

upper_bound ((dist_min P) .: R) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

R is non empty Element of K6( the carrier of (TopSpaceMetr n))

max_dist_min (R,P) is V11() real ext-real Element of REAL

(n,P,Q) is V11() real ext-real Element of REAL

max_dist_min (P,Q) is V11() real ext-real Element of REAL

max_dist_min (Q,P) is V11() real ext-real Element of REAL

max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL

(n,Q,R) is V11() real ext-real Element of REAL

max_dist_min (Q,R) is V11() real ext-real Element of REAL

max_dist_min (R,Q) is V11() real ext-real Element of REAL

max ((max_dist_min (Q,R)),(max_dist_min (R,Q))) is V11() real ext-real Element of REAL

(n,P,Q) + (n,Q,R) is V11() real ext-real Element of REAL

dist_min R is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist_min R) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

P1 is non empty V45() V46() V47() Element of K6(REAL)

Q1 is V11() real ext-real set

dom (dist_min R) is Element of K6( the carrier of (TopSpaceMetr n))

R1 is set

(dist_min R) . R1 is V11() real ext-real set

the carrier of n is non empty set

y is Element of the carrier of n

(dist_min R) . y is V11() real ext-real set

((dist_min R) . y) - (n,Q,R) is V11() real ext-real Element of REAL

z is Element of the carrier of n

dist (y,z) is V11() real ext-real Element of REAL

(dist_min R) . z is V11() real ext-real set

(dist (y,z)) + ((dist_min R) . z) is V11() real ext-real Element of REAL

(dist (y,z)) + (n,Q,R) is V11() real ext-real Element of REAL

dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

(dist_min Q) . y is V11() real ext-real set

upper_bound P1 is V11() real ext-real Element of REAL

[#] ((dist_min R) .: P) is V45() V46() V47() Element of K6(REAL)

upper_bound ([#] ((dist_min R) .: P)) is V11() real ext-real Element of REAL

upper_bound ((dist_min R) .: P) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

(n,P,Q) is V11() real ext-real Element of REAL

max_dist_min (P,Q) is V11() real ext-real Element of REAL

max_dist_min (Q,P) is V11() real ext-real Element of REAL

max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

(n,P,P) is V11() real ext-real Element of REAL

max_dist_min (P,P) is V11() real ext-real Element of REAL

max ((max_dist_min (P,P)),(max_dist_min (P,P))) is V11() real ext-real Element of REAL

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

(n,P,Q) is V11() real ext-real Element of REAL

max_dist_min (P,Q) is V11() real ext-real Element of REAL

max_dist_min (Q,P) is V11() real ext-real Element of REAL

max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL

dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set

K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set

(dist_min Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)

upper_bound ((dist_min Q) .: P) is V11() real ext-real Element of REAL

R is non empty V45() V46() V47() Element of K6(REAL)

upper_bound R is V11() real ext-real Element of REAL

P1 is set

the carrier of n is non empty set

dom (dist_min Q) is Element of K6( the carrier of (TopSpaceMetr n))

(dist_min Q) . P1 is V11() real ext-real set

Q1 is Element of the carrier of n

P1 is set

the carrier of n is non empty set

dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))

(dist_min P) .: Q is non empty V45() V46() V47() Element of K6( the carrier of R^1)

upper_bound ((dist_min P) .: Q) is V11() real ext-real Element of REAL

R1 is non empty V45() V46() V47() Element of K6(REAL)

upper_bound R1 is V11() real ext-real Element of REAL

dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))

(dist_min P) . P1 is V11() real ext-real set

Q1 is Element of the carrier of n

n is non empty Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr n) is non empty set

K6( the carrier of (TopSpaceMetr n)) is non empty set

P is non empty Element of K6( the carrier of (TopSpaceMetr n))

Q is non empty Element of K6( the carrier of (TopSpaceMetr n))

R is non empty Element of K6( the carrier of (TopSpaceMetr n))

(n,P,R) is V11() real ext-real Element of REAL

max_dist_min (P,R) is V11() real ext-real Element of REAL

max_dist_min (R,P) is V11() real ext-real Element of REAL

max ((max_dist_min (P,R)),(max_dist_min (R,P))) is V11() real ext-real Element of REAL

(n,P,Q) is V11() real ext-real Element of REAL

max_dist_min (P,Q) is V11() real ext-real Element of REAL

max_dist_min (Q,P) is V11() real ext-real Element of REAL

max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL

(n,Q,R) is V11() real ext-real Element of REAL

max_dist_min (Q,R) is V11() real ext-real Element of REAL

max_dist_min (R,Q) is V11() real ext-real Element of REAL

max ((max_dist_min (Q,R)),(max_dist_min (R,Q))) is V11() real ext-real Element of REAL

(n,P,Q) + (n,Q,R) is V11() real ext-real Element of REAL

n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()

the carrier of (TOP-REAL n) is non empty set

K6( the carrier of (TOP-REAL n)) is non empty set

Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set

P is Element of K6( the carrier of (TOP-REAL n))

Q is Element of K6( the carrier of (TOP-REAL n))

the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))

K6(K6( the carrier of (TOP-REAL n))) is non empty set

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

R is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

P1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

max_dist_min (R,P1) is V11() real ext-real Element of REAL

Q1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

R1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

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

max_dist_min (Q1,R1) is V11() real ext-real Element of REAL

y is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

z is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

P1 is V11() real ext-real Element of REAL

max_dist_min (y,z) is V11() real ext-real Element of REAL

n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()

the carrier of (TOP-REAL n) is non empty set

K6( the carrier of (TOP-REAL n)) is non empty set

Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set

P is Element of K6( the carrier of (TOP-REAL n))

Q is Element of K6( the carrier of (TOP-REAL n))

the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))

K6(K6( the carrier of (TOP-REAL n))) is non empty set

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

R is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

P1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

((Euclid n),R,P1) is V11() real ext-real Element of REAL

max_dist_min (R,P1) is V11() real ext-real Element of REAL

max_dist_min (P1,R) is V11() real ext-real Element of REAL

max ((max_dist_min (R,P1)),(max_dist_min (P1,R))) is V11() real ext-real Element of REAL

Q1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

R1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

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

((Euclid n),Q1,R1) is V11() real ext-real Element of REAL

max_dist_min (Q1,R1) is V11() real ext-real Element of REAL

max_dist_min (R1,Q1) is V11() real ext-real Element of REAL

max ((max_dist_min (Q1,R1)),(max_dist_min (R1,Q1))) is V11() real ext-real Element of REAL

y is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

z is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

P1 is V11() real ext-real Element of REAL

((Euclid n),y,z) is V11() real ext-real Element of REAL

max_dist_min (y,z) is V11() real ext-real Element of REAL

max_dist_min (z,y) is V11() real ext-real Element of REAL

max ((max_dist_min (y,z)),(max_dist_min (z,y))) is V11() real ext-real Element of REAL

P1 is Element of K6( the carrier of (TOP-REAL n))

R1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

Q1 is Element of K6( the carrier of (TOP-REAL n))

y is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

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

((Euclid n),R1,y) is V11() real ext-real Element of REAL

max_dist_min (R1,y) is V11() real ext-real Element of REAL

max_dist_min (y,R1) is V11() real ext-real Element of REAL

max ((max_dist_min (R1,y)),(max_dist_min (y,R1))) is V11() real ext-real Element of REAL

n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()

the carrier of (TOP-REAL n) is non empty set

K6( the carrier of (TOP-REAL n)) is non empty set

P is non empty Element of K6( the carrier of (TOP-REAL n))

Q is non empty Element of K6( the carrier of (TOP-REAL n))

(n,P,Q) is V11() real ext-real Element of REAL

the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))

K6(K6( the carrier of (TOP-REAL n))) is non empty set

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set

R is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

P1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

((Euclid n),R,P1) is V11() real ext-real Element of REAL

max_dist_min (R,P1) is V11() real ext-real Element of REAL

max_dist_min (P1,R) is V11() real ext-real Element of REAL

max ((max_dist_min (R,P1)),(max_dist_min (P1,R))) is V11() real ext-real Element of REAL

n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()

the carrier of (TOP-REAL n) is non empty set

K6( the carrier of (TOP-REAL n)) is non empty set

P is non empty Element of K6( the carrier of (TOP-REAL n))

(n,P,P) is V11() real ext-real Element of REAL

the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))

K6(K6( the carrier of (TOP-REAL n))) is non empty set

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set

Q is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

((Euclid n),Q,Q) is V11() real ext-real Element of REAL

max_dist_min (Q,Q) is V11() real ext-real Element of REAL

max ((max_dist_min (Q,Q)),(max_dist_min (Q,Q))) is V11() real ext-real Element of REAL

n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()

the carrier of (TOP-REAL n) is non empty set

K6( the carrier of (TOP-REAL n)) is non empty set

P is non empty Element of K6( the carrier of (TOP-REAL n))

Q is non empty Element of K6( the carrier of (TOP-REAL n))

(n,P,Q) is V11() real ext-real Element of REAL

the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))

K6(K6( the carrier of (TOP-REAL n))) is non empty set

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set

R is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

P1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

((Euclid n),R,P1) is V11() real ext-real Element of REAL

max_dist_min (R,P1) is V11() real ext-real Element of REAL

max_dist_min (P1,R) is V11() real ext-real Element of REAL

max ((max_dist_min (R,P1)),(max_dist_min (P1,R))) is V11() real ext-real Element of REAL

n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT

TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()

the carrier of (TOP-REAL n) is non empty set

K6( the carrier of (TOP-REAL n)) is non empty set

P is non empty Element of K6( the carrier of (TOP-REAL n))

Q is non empty Element of K6( the carrier of (TOP-REAL n))

R is non empty Element of K6( the carrier of (TOP-REAL n))

(n,P,R) is V11() real ext-real Element of REAL

(n,P,Q) is V11() real ext-real Element of REAL

(n,Q,R) is V11() real ext-real Element of REAL

(n,P,Q) + (n,Q,R) is V11() real ext-real Element of REAL

the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))

K6(K6( the carrier of (TOP-REAL n))) is non empty set

TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct

Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct

the carrier of (TopSpaceMetr (Euclid n)) is non empty set

K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set

R1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

Q1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

((Euclid n),Q1,R1) is V11() real ext-real Element of REAL

max_dist_min (Q1,R1) is V11() real ext-real Element of REAL

max_dist_min (R1,Q1) is V11() real ext-real Element of REAL

max ((max_dist_min (Q1,R1)),(max_dist_min (R1,Q1))) is V11() real ext-real Element of REAL

P1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))

((Euclid n),P1,R1) is V11() real ext-real Element of REAL

max_dist_min (P1,R1) is V11() real ext-real Element of REAL

max_dist_min (R1,P1) is V11() real ext-real Element of REAL

max ((max_dist_min (P1,R1)),(max_dist_min (R1,P1))) is V11() real ext-real Element of REAL

((Euclid n),P1,Q1) is V11() real ext-real Element of REAL

max_dist_min (P1,Q1) is V11() real ext-real Element of REAL

max_dist_min (Q1,P1) is V11() real ext-real Element of REAL

max ((max_dist_min (P1,Q1)),(max_dist_min (Q1,P1))) is V11() real ext-real Element of REAL