:: SIMPLEX2 semantic presentation

REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V109() non bounded_below non bounded_above interval set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() left_end bounded_below Element of bool REAL

bool REAL is non empty non trivial non finite set

1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

- 1 is non empty real V55() ext-real non positive negative set

K165(1) is real integer finite V55() ext-real non positive set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() left_end bounded_below set

bool omega is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

COMPLEX is non empty non trivial non finite complex-membered V109() set

RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V109() set

INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V109() set

[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite V93() set

bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite V93() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set

[:REAL,REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

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

[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

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

[:RAT,RAT:] is non empty non trivial Relation-like RAT -valued non finite V93() V94() V95() set

bool [:RAT,RAT:] is non empty non trivial non finite set

[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like RAT -valued non finite V93() V94() V95() set

bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set

[:INT,INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V93() V94() V95() set

bool [:INT,INT:] is non empty non trivial non finite set

[:[:INT,INT:],INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V93() V94() V95() set

bool [:[:INT,INT:],INT:] is non empty non trivial non finite set

[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V93() V94() V95() V96() set

[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V93() V94() V95() V96() set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed set

2 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

[:1,1:] is non empty Relation-like RAT -valued INT -valued finite V93() V94() V95() V96() set

bool [:1,1:] is non empty finite finite-membered set

[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued finite V93() V94() V95() V96() set

bool [:[:1,1:],1:] is non empty finite finite-membered set

[:[:1,1:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

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

[:2,2:] is non empty Relation-like RAT -valued INT -valued finite V93() V94() V95() V96() set

[:[:2,2:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

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

TOP-REAL 2 is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()

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

K523() is non empty V128() L9()

the carrier of K523() is non empty set

K528() is non empty V128() V201() V202() V203() V205() V231() V232() V233() V234() V235() V236() L9()

K529() is non empty V128() V203() V205() V234() V235() V236() M21(K528())

K530() is non empty V128() V201() V203() V205() V234() V235() V236() V237() M24(K528(),K529())

K532() is non empty V128() V201() V203() V205() L9()

K533() is non empty V128() V201() V203() V205() V237() M21(K532())

ExtREAL is non empty ext-real-membered interval set

[:NAT,REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

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

K743() is non empty strict TopSpace-like T_0 T_1 T_2 compact real-membered TopStruct

the carrier of K743() is non empty complex-membered ext-real-membered real-membered set

RealSpace is strict real-membered MetrStruct

real_dist is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:REAL,REAL:],REAL:]

MetrStruct(# REAL,real_dist #) is strict MetrStruct

R^1 is non empty strict TopSpace-like real-membered TopStruct

the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set

[:COMPLEX,REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:COMPLEX,REAL:] is non empty non trivial non finite set

K844() is set

{{}} is non empty trivial functional finite finite-membered 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set

{{}} * is non empty functional FinSequence-membered FinSequenceSet of {{}}

[:({{}} *),{{}}:] is non empty Relation-like RAT -valued INT -valued V93() V94() V95() V96() set

bool [:({{}} *),{{}}:] is non empty set

PFuncs (({{}} *),{{}}) is set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() V56() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed Element of NAT

Euclid 0 is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct

REAL 0 is non empty functional FinSequence-membered FinSequenceSet of REAL

0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

Pitag_dist 0 is non empty Relation-like [:(REAL 0),(REAL 0):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL 0),(REAL 0):],REAL:]

[:(REAL 0),(REAL 0):] is non empty Relation-like set

[:[:(REAL 0),(REAL 0):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:[:(REAL 0),(REAL 0):],REAL:] is non empty non trivial non finite set

MetrStruct(# (REAL 0),(Pitag_dist 0) #) is strict MetrStruct

TopSpaceMetr (Euclid 0) is non empty trivial finite 1 -element strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 compact metrizable TopStruct

the carrier of (Euclid 0) is non empty set

Family_open_set (Euclid 0) is Element of bool (bool the carrier of (Euclid 0))

bool the carrier of (Euclid 0) is non empty set

bool (bool the carrier of (Euclid 0)) is non empty set

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

3 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

bool the carrier of R^1 is non empty set

-infty is non empty non real ext-real non positive negative set

TOP-REAL 1 is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()

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

[: the carrier of (TOP-REAL 1), the carrier of R^1:] is non empty Relation-like V93() V94() V95() set

bool [: the carrier of (TOP-REAL 1), the carrier of R^1:] is non empty set

+infty is non empty non real ext-real positive non negative set

union {} is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

n is non empty Reflexive discerning V181() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct

the carrier of n is non empty set

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

bool the carrier of n is non empty set

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

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

the carrier of (TopSpaceMetr n) is non empty set

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

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

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

C is Element of bool (bool the carrier of (TopSpaceMetr n))

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

E is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

C is Element of the carrier of n

Ball (C,E) is bounded Element of bool the carrier of n

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

Funcs (([#] (TopSpaceMetr n)),REAL) is non empty functional FUNCTION_DOMAIN of [#] (TopSpaceMetr n), REAL

n1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng n1 is finite set

[: the carrier of (TopSpaceMetr n), the carrier of R^1:] is non empty Relation-like V93() V94() V95() set

bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:] is non empty set

union C is Element of bool the carrier of (TopSpaceMetr n)

len n1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

dom n1 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT

n1 . 1 is set

c is Element of bool the carrier of (TopSpaceMetr n)

c ` is Element of bool the carrier of (TopSpaceMetr n)

the carrier of (TopSpaceMetr n) \ c is set

(c `) ` is Element of bool the carrier of (TopSpaceMetr n)

the carrier of (TopSpaceMetr n) \ (c `) is set

TRC is non empty closed Element of bool the carrier of (TopSpaceMetr n)

dist_min TRC is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

f is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL

n1 . (f + 1) is set

R is Relation-like [#] (TopSpaceMetr n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of Funcs (([#] (TopSpaceMetr n)),REAL)

G is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

G0 is Relation-like [#] (TopSpaceMetr n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of Funcs (([#] (TopSpaceMetr n)),REAL)

p is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

h is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

G is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

G0 is Element of bool the carrier of (TopSpaceMetr n)

G0 ` is Element of bool the carrier of (TopSpaceMetr n)

the carrier of (TopSpaceMetr n) \ G0 is set

(G0 `) ` is Element of bool the carrier of (TopSpaceMetr n)

the carrier of (TopSpaceMetr n) \ (G0 `) is set

p is non empty Element of bool the carrier of (TopSpaceMetr n)

dist_min p is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

h is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

h is Relation-like [#] (TopSpaceMetr n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of Funcs (([#] (TopSpaceMetr n)),REAL)

gx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

cgx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

p ` is Element of bool the carrier of (TopSpaceMetr n)

the carrier of (TopSpaceMetr n) \ p is set

GX is Element of the carrier of (TopSpaceMetr n)

cgx . GX is real V55() ext-real Element of the carrier of R^1

gx . GX is real V55() ext-real Element of the carrier of R^1

(dist_min p) . GX is real V55() ext-real Element of the carrier of R^1

max ((gx . GX),((dist_min p) . GX)) is real V55() ext-real set

G is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

carr is Relation-like [#] (TopSpaceMetr n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of Funcs (([#] (TopSpaceMetr n)),REAL)

f is Relation-like NAT -defined Funcs (([#] (TopSpaceMetr n)),REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (([#] (TopSpaceMetr n)),REAL)

len f is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

f /. 1 is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

dom f is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT

f /. (len f) is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

R is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

rng R is non empty complex-membered ext-real-membered real-membered Element of bool REAL

G is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1

[#] G is complex-membered ext-real-membered real-membered Element of bool REAL

p is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

f /. p is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL

f /. (p + 1) is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

h is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

h is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

f /. h is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

gx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

cgx is Element of the carrier of (TopSpaceMetr n)

gx . cgx is real V55() ext-real Element of the carrier of R^1

h . cgx is real V55() ext-real Element of the carrier of R^1

p - 1 is real integer finite V55() ext-real Element of REAL

K163(p,K165(1)) is real integer finite V55() ext-real set

h is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

h + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL

gx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

n1 . (p + 1) is set

cgx is non empty Element of bool the carrier of (TopSpaceMetr n)

cgx ` is Element of bool the carrier of (TopSpaceMetr n)

the carrier of (TopSpaceMetr n) \ cgx is set

dist_min cgx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

GX is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

f /. GX is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

I is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

t is Element of the carrier of (TopSpaceMetr n)

I . t is real V55() ext-real Element of the carrier of R^1

h . t is real V55() ext-real Element of the carrier of R^1

gx . t is real V55() ext-real Element of the carrier of R^1

(dist_min cgx) . t is real V55() ext-real Element of the carrier of R^1

max ((gx . t),((dist_min cgx) . t)) is real V55() ext-real set

f /. {} is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

p is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

h is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

h is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

f /. h is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

gx is Element of the carrier of (TopSpaceMetr n)

h . gx is real V55() ext-real Element of the carrier of R^1

p . gx is real V55() ext-real Element of the carrier of R^1

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

R .: ([#] (TopSpaceMetr n)) is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1

p is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of bool REAL

lower_bound p is real V55() ext-real Element of REAL

inf p is real V55() ext-real set

h is set

R . h is real V55() ext-real set

gx is set

GX is set

n1 . GX is set

I is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

cgx is Element of the carrier of (TopSpaceMetr n)

(dist_min TRC) . cgx is real V55() ext-real Element of the carrier of R^1

I - 1 is real integer finite V55() ext-real Element of REAL

K163(I,K165(1)) is real integer finite V55() ext-real set

t is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

f /. t is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

f /. I is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

t + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL

y is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

x is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

t + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL

n1 . (t + 1) is set

i1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

i2 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

n1 . I is set

i1 is non empty Element of bool the carrier of (TopSpaceMetr n)

i1 ` is Element of bool the carrier of (TopSpaceMetr n)

the carrier of (TopSpaceMetr n) \ i1 is set

dist_min i1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

cgx is Element of the carrier of (TopSpaceMetr n)

(dist_min i1) . cgx is real V55() ext-real Element of the carrier of R^1

x . cgx is real V55() ext-real Element of the carrier of R^1

y . cgx is real V55() ext-real Element of the carrier of R^1

max ((y . cgx),((dist_min i1) . cgx)) is real V55() ext-real set

t is non empty real V55() ext-real positive non negative Element of REAL

y is Element of the carrier of n

Ball (y,t) is bounded Element of bool the carrier of n

R . y is real V55() ext-real set

x is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

x . y is real V55() ext-real set

x is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

f /. x is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

i1 is set

i2 is Element of the carrier of n

dist (y,i2) is real V55() ext-real non negative Element of REAL

the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]

[: the carrier of n, the carrier of n:] is non empty Relation-like set

[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set

the distance of n . (y,i2) is real V55() ext-real Element of REAL

(dist_min TRC) . y is real V55() ext-real set

x - 1 is real integer finite V55() ext-real Element of REAL

K163(x,K165(1)) is real integer finite V55() ext-real set

i1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

f /. i1 is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)

i1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL

i2 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

S2 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

i1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL

n1 . (i1 + 1) is set

bb1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

bb2 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

n1 . x is set

bb1 is non empty Element of bool the carrier of (TopSpaceMetr n)

bb1 ` is Element of bool the carrier of (TopSpaceMetr n)

the carrier of (TopSpaceMetr n) \ bb1 is set

dist_min bb1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

bb2 is set

r is Element of the carrier of n

(dist_min bb1) . y is real V55() ext-real set

dist (y,r) is real V55() ext-real non negative Element of REAL

the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]

[: the carrier of n, the carrier of n:] is non empty Relation-like set

[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set

the distance of n . (y,r) is real V55() ext-real Element of REAL

S2 . y is real V55() ext-real set

i2 . y is real V55() ext-real set

max ((i2 . y),((dist_min bb1) . y)) is real V55() ext-real set

r1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]

r1 . y is real V55() ext-real set

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

n is non empty Reflexive discerning V181() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct

the carrier of n is non empty set

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

bool the carrier of n is non empty set

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

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

the carrier of (TopSpaceMetr n) is non empty set

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

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

T is open Element of bool (bool the carrier of (TopSpaceMetr n))

I is open Element of bool (bool the carrier of (TopSpaceMetr n))

C is non empty real V55() ext-real positive non negative (n,T)

E is Element of the carrier of n

Ball (E,C) is bounded Element of bool the carrier of n

C is Element of bool the carrier of (TopSpaceMetr n)

union T is Element of bool the carrier of (TopSpaceMetr n)

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

union I is Element of bool the carrier of (TopSpaceMetr n)

n is non empty Reflexive discerning V181() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct

the carrier of n is non empty set

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

bool the carrier of n is non empty set

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

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

the carrier of (TopSpaceMetr n) is non empty set

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

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

T is open Element of bool (bool the carrier of (TopSpaceMetr n))

I is open Element of bool (bool the carrier of (TopSpaceMetr n))

C is non empty real V55() ext-real positive non negative (n,T)

C is Element of the carrier of n

Ball (C,C) is bounded Element of bool the carrier of n

n1 is Element of bool the carrier of (TopSpaceMetr n)

c is set

TRC is Element of bool the carrier of (TopSpaceMetr n)

carr is Element of bool the carrier of (TopSpaceMetr n)

union T is Element of bool the carrier of (TopSpaceMetr n)

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

union I is Element of bool the carrier of (TopSpaceMetr n)

n is non empty Reflexive discerning V181() triangle MetrStruct

TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct

the carrier of n is non empty set

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

bool the carrier of n is non empty set

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

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

the carrier of (TopSpaceMetr n) is non empty set

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

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

T is open Element of bool (bool the carrier of (TopSpaceMetr n))

I is non empty real V55() ext-real positive non negative (n,T)

C is non empty real V55() ext-real positive non negative Element of REAL

E is Element of the carrier of n

Ball (E,I) is bounded Element of bool the carrier of n

C is Element of bool the carrier of (TopSpaceMetr n)

Ball (E,C) is bounded Element of bool the carrier of n

n1 is Element of bool the carrier of (TopSpaceMetr n)

n is non empty Reflexive MetrStruct

the carrier of n is non empty set

bool the carrier of n is non empty set

T is Element of bool the carrier of n

I is non empty finite Element of bool the carrier of n

C is set

{ H

C is Element of the carrier of n

dist (C,C) is real V55() ext-real Element of REAL

the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]

[: the carrier of n, the carrier of n:] is non empty Relation-like set

[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set

the distance of n . (C,C) is real V55() ext-real Element of REAL

n1 is set

c is Element of the carrier of n

TRC is Element of the carrier of n

dist (c,TRC) is real V55() ext-real Element of REAL

the distance of n . (c,TRC) is real V55() ext-real Element of REAL

n1 is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

sup n1 is real V55() ext-real set

c is real V55() ext-real Element of REAL

c + 1 is real V55() ext-real Element of REAL

TRC is real V55() ext-real Element of REAL

carr is Element of the carrier of n

f is Element of the carrier of n

dist (carr,f) is real V55() ext-real Element of REAL

the distance of n . (carr,f) is real V55() ext-real Element of REAL

n is non empty Reflexive MetrStruct

the carrier of n is non empty set

bool the carrier of n is non empty set

T is non empty finite bounded Element of bool the carrier of n

diameter T is real V55() ext-real Element of REAL

the Element of T is Element of T

{ H

C is set

n1 is Element of the carrier of n

c is Element of the carrier of n

dist (n1,c) is real V55() ext-real Element of REAL

the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]

[: the carrier of n, the carrier of n:] is non empty Relation-like set

[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set

the distance of n . (n1,c) is real V55() ext-real Element of REAL

C is Element of the carrier of n

dist (C,C) is real V55() ext-real Element of REAL

the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]

[: the carrier of n, the carrier of n:] is non empty Relation-like set

[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set

the distance of n . (C,C) is real V55() ext-real Element of REAL

C is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set

sup C is real V55() ext-real set

n1 is real V55() ext-real Element of REAL

c is Element of the carrier of n

TRC is Element of the carrier of n

dist (c,TRC) is real V55() ext-real Element of REAL

the distance of n . (c,TRC) is real V55() ext-real Element of REAL

carr is Element of the carrier of n

f is Element of the carrier of n

dist (carr,f) is real V55() ext-real Element of REAL

the distance of n . (carr,f) is real V55() ext-real Element of REAL

n is non empty Reflexive MetrStruct

the carrier of n is non empty set

bool the carrier of n is non empty set

T is Element of bool the carrier of n

I is non void TopStruct

the carrier of I is set

bool the carrier of I is non empty set

the topology of I is open Element of bool (bool the carrier of I)

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

C is real V55() ext-real set

T is set

n is non empty Reflexive MetrStruct

the carrier of n is non empty set

the Element of the carrier of n is Element of the carrier of n

bool T is non empty set

{} T is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed Element of bool T

{({} T)} is non empty trivial functional finite finite-membered 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded V365(T) Element of bool (bool T)

bool (bool T) is non empty set

Complex_of {({} T)} is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total SimplicialComplexStr of T

subset-closed_closure_of {({} T)} is non empty finite-membered non with_non-empty_elements subset-closed Element of bool (bool T)

TopStruct(# T,(subset-closed_closure_of {({} T)}) #) is strict TopStruct

C is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total SimplicialComplexStr of T

{} n is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed bounded Element of bool the carrier of n

bool the carrier of n is non empty set

diameter ({} n) is real V55() ext-real Element of REAL

the topology of C is finite finite-membered V365( the carrier of C) open Element of bool (bool the carrier of C)

the carrier of C is set

bool the carrier of C is non empty set

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

E is real V55() ext-real Element of REAL

C is Element of bool the carrier of n

diameter C is real V55() ext-real Element of REAL

bool ({} T) is non empty finite finite-membered V365( {} T) Element of bool (bool ({} T))

bool ({} T) is non empty finite finite-membered set

bool (bool ({} T)) is non empty finite finite-membered set

n is non empty Reflexive MetrStruct

the set is set

the non void subset-closed finite-membered non with_non-empty_elements (n) SimplicialComplexStr of the set is non void subset-closed finite-membered non with_non-empty_elements (n) SimplicialComplexStr of the set

n is non empty Reflexive MetrStruct

T is set

I is (n) SimplicialComplexStr of T

C is subset-closed finite-membered SubSimplicialComplex of I

the topology of C is finite-membered open Element of bool (bool the carrier of C)

the carrier of C is set

bool the carrier of C is non empty set

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

the topology of I is open Element of bool (bool the carrier of I)

the carrier of I is set

bool the carrier of I is non empty set

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

the carrier of n is non empty set

bool the carrier of n is non empty set

E is real V55() ext-real set

C is Element of bool the carrier of n

diameter C is real V55() ext-real Element of REAL

n is non empty Reflexive MetrStruct

T is set

I is subset-closed (n) SimplicialComplexStr of T

C is real integer finite V55() ext-real set

Skeleton_of (I,C) is subset-closed finite-membered finite-degree (n) SubSimplicialComplex of I

the carrier of I is set

the topology of I is open Element of bool (bool the carrier of I)

bool the carrier of I is non empty set

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

C + 1 is real V55() ext-real set

K163(C,1) is real integer finite V55() ext-real set

the_subsets_with_limited_card ((C + 1), the topology of I, the carrier of I) is Element of bool (bool the carrier of I)

Complex_of (the_subsets_with_limited_card ((C + 1), the topology of I, the carrier of I)) is strict subset-closed total SimplicialComplexStr of the carrier of I

subset-closed_closure_of (the_subsets_with_limited_card ((C + 1), the topology of I, the carrier of I)) is subset-closed Element of bool (bool the carrier of I)

TopStruct(# the carrier of I,(subset-closed_closure_of (the_subsets_with_limited_card ((C + 1), the topology of I, the carrier of I))) #) is strict TopStruct

n is non empty Reflexive MetrStruct

T is TopStruct

Vertices T is Element of bool the carrier of T

the carrier of T is set

bool the carrier of T is non empty set

the carrier of n is non empty set

bool the carrier of n is non empty set

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

(Vertices T) /\ ([#] n) is Element of bool the carrier of n

C is finite bounded Element of bool the carrier of n

diameter C is real V55() ext-real Element of REAL

the topology of T is open Element of bool (bool the carrier of T)

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

E is Element of bool the carrier of n

diameter E is real V55() ext-real Element of REAL

C is Element of bool the carrier of T

n is non empty Reflexive MetrStruct

T is TopStruct

the topology of T is open Element of bool (bool the carrier of T)

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

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

the carrier of n is non empty set

bool the carrier of n is non empty set

bool ([#] n) is non empty Element of bool (bool ([#] n))

bool ([#] n) is non empty set

bool (bool ([#] n)) is non empty set

{ H

C is set

E is Element of bool the carrier of n

diameter E is real V55() ext-real Element of REAL

E is set

n1 is real V55() ext-real set

c is ext-real set

C is complex-membered ext-real-membered real-membered set

TRC is Element of bool the carrier of n

diameter TRC is real V55() ext-real Element of REAL

C is Element of bool the carrier of n

diameter C is real V55() ext-real Element of REAL

sup C is ext-real set

c is real V55() ext-real Element of REAL

TRC is Element of bool the carrier of n

diameter TRC is real V55() ext-real Element of REAL

TRC is real V55() ext-real set

carr is ext-real set

f is Element of bool the carrier of n

diameter f is real V55() ext-real Element of REAL

I is real V55() ext-real Element of REAL

I is real V55() ext-real Element of REAL

C is real V55() ext-real Element of REAL

I is real V55() ext-real Element of REAL

C is real V55() ext-real Element of REAL

E is real V55() ext-real Element of REAL

C is real V55() ext-real Element of REAL

n is non empty Reflexive MetrStruct

T is TopStruct

(n,T) is real V55() ext-real Element of REAL

the topology of T is open Element of bool (bool the carrier of T)

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

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

the carrier of n is non empty set

bool the carrier of n is non empty set

bool ([#] n) is non empty Element of bool (bool ([#] n))

bool ([#] n) is non empty set

bool (bool ([#] n)) is non empty set

I is set

C is Element of bool the carrier of n

diameter C is real V55() ext-real Element of REAL

E is real V55() ext-real set

the topology of T is open Element of bool (bool the carrier of T)

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

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

the carrier of n is non empty set

bool the carrier of n is non empty set

bool ([#] n) is non empty Element of bool (bool ([#] n))

bool ([#] n) is non empty set

bool (bool ([#] n)) is non empty set

the topology of T is open Element of bool (bool the carrier of T)

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

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

the carrier of n is non empty set

bool the carrier of n is non empty set

bool ([#] n) is non empty Element of bool (bool ([#] n))

bool ([#] n) is non empty set

bool (bool ([#] n)) is non empty set

n is set

T is non empty Reflexive MetrStruct

I is (T) SimplicialComplexStr of n

(T,I) is real V55() ext-real Element of REAL

C is subset-closed finite-membered (T) SubSimplicialComplex of I

(T,C) is real V55() ext-real Element of REAL

the topology of C is finite-membered open Element of bool (bool the carrier of C)

the carrier of C is set

bool the carrier of C is non empty set

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

the topology of I is open Element of bool (bool the carrier of I)

the carrier of I is set

bool the carrier of I is non empty set

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

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

the carrier of T is non empty set

bool the carrier of T is non empty set

bool ([#] T) is non empty Element of bool (bool ([#] T))

bool ([#] T) is non empty set

bool (bool ([#] T)) is non empty set

E is Element of bool the carrier of T

diameter E is real V55() ext-real Element of REAL

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

the carrier of T is non empty set

bool the carrier of T is non empty set

bool ([#] T) is non empty Element of bool (bool ([#] T))

bool ([#] T) is non empty set

bool (bool ([#] T)) is non empty set

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

the carrier of T is non empty set

bool the carrier of T is non empty set

bool ([#] T) is non empty Element of bool (bool ([#] T))

bool ([#] T) is non empty set

bool (bool ([#] T)) is non empty set

n is set

T is non empty Reflexive MetrStruct

the real V55() ext-real Element of REAL is real V55() ext-real Element of REAL

C is subset-closed (T) SimplicialComplexStr of n

(T,C) is real V55() ext-real Element of REAL

E is real integer finite V55() ext-real set

Skeleton_of (C,E) is subset-closed finite-membered finite-degree (T) SubSimplicialComplex of C

the carrier of C is set

the topology of C is open Element of bool (bool the carrier of C)

bool the carrier of C is non empty set

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

E + 1 is real V55() ext-real set

K163(E,1) is real integer finite V55() ext-real set

the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C) is Element of bool (bool the carrier of C)

Complex_of (the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C)) is strict subset-closed total SimplicialComplexStr of the carrier of C

subset-closed_closure_of (the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C)) is subset-closed Element of bool (bool the carrier of C)

TopStruct(# the carrier of C,(subset-closed_closure_of (the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C))) #) is strict TopStruct

(T,(Skeleton_of (C,E))) is real V55() ext-real Element of REAL

the topology of (Skeleton_of (C,E)) is finite-membered open Element of bool (bool the carrier of (Skeleton_of (C,E)))

the carrier of (Skeleton_of (C,E)) is set

bool the carrier of (Skeleton_of (C,E)) is non empty set

bool (bool the carrier of (Skeleton_of (C,E))) is non empty set

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

the carrier of T is non empty set

bool the carrier of T is non empty set

bool ([#] T) is non empty Element of bool (bool ([#] T))

bool ([#] T) is non empty set

bool (bool ([#] T)) is non empty set

the_family_of C is Element of bool (bool the carrier of C)

n1 is Element of bool the carrier of T

E + 1 is real integer finite V55() ext-real Element of REAL

the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C) is finite-membered Element of bool (bool the carrier of C)

c is set

TRC is Element of bool the carrier of C

diameter n1 is real V55() ext-real Element of REAL

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

the carrier of T is non empty set

bool the carrier of T is non empty set

bool ([#] T) is non empty Element of bool (bool ([#] T))

bool ([#] T) is non empty set

bool (bool ([#] T)) is non empty set

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

the carrier of T is non empty set

bool the carrier of T is non empty set

bool ([#] T) is non empty Element of bool (bool ([#] T))

bool ([#] T) is non empty set

bool (bool ([#] T)) is non empty set

n is non empty Reflexive MetrStruct

T is non void subset-closed non with_non-empty_elements (n) TopStruct

(n,T) is real V55() ext-real Element of REAL

the carrier of n is non empty set

bool the carrier of n is non empty set

the carrier of T is set

bool the carrier of T is non empty set

I is real V55() ext-real Element of REAL

{} T is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() open compact ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed Element of bool the carrier of T

{} n is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed bounded Element of bool the carrier of n

the topology of T is open Element of bool (bool the carrier of T)

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

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

bool ([#] n) is non empty Element of bool (bool ([#] n))

bool ([#] n) is non empty set

bool (bool ([#] n)) is non empty set

C is Element of bool the carrier of n

diameter C is real V55() ext-real Element of REAL

C is real V55() ext-real set

E is Element of bool the carrier of n

diameter E is real V55() ext-real Element of REAL

C is Element of bool the carrier of n

diameter C is real V55() ext-real Element of REAL

C is Element of bool the carrier of n

diameter C is real V55() ext-real Element of REAL

n is non empty Reflexive MetrStruct

the carrier of n is non empty set

bool the carrier of n is non empty set

T is finite bounded Element of bool the carrier of n

{T} is non empty trivial finite finite-membered 1 -element V365( the carrier of n) Element of bool (bool the carrier of n)

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

Complex_of {T} is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total SimplicialComplexStr of the carrier of n

subset-closed_closure_of {T} is non empty finite-membered non with_non-empty_elements subset-closed Element of bool (bool the carrier of n)

TopStruct(# the carrier of n,(subset-closed_closure_of {T}) #) is non empty strict TopStruct

(n,(Complex_of {T})) is real V55() ext-real Element of REAL

diameter T is real V55() ext-real Element of REAL

C is non void subset-closed finite-membered non with_non-empty_elements (n) SimplicialComplexStr of the carrier of n

the carrier of C is set

bool the carrier of C is non empty set

the topology of C is finite-membered open Element of bool (bool the carrier of C)

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

bool T is non empty finite finite-membered V365(T) Element of bool (bool T)

bool T is non empty finite finite-membered set

bool (bool T) is non empty finite finite-membered set

C is Element of bool the carrier of n

diameter C is real V55() ext-real Element of REAL

(n,C) is real V55() ext-real Element of REAL

E is Element of bool the carrier of C

n is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

TOP-REAL n is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()

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

Euclid n is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

Pitag_dist n is non empty Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL n),(REAL n):],REAL:]

[:(REAL n),(REAL n):] is non empty Relation-like set

[:[:(REAL n),(REAL n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:[:(REAL n),(REAL n):],REAL:] is non empty non trivial non finite set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

T is SimplicialComplexStr of the carrier of (TOP-REAL n)

((Euclid n),T) is real V55() ext-real Element of REAL

n is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

TOP-REAL n is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()

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

Euclid n is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

Pitag_dist n is non empty Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL n),(REAL n):],REAL:]

[:(REAL n),(REAL n):] is non empty Relation-like set

[:[:(REAL n),(REAL n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:[:(REAL n),(REAL n):],REAL:] is non empty non trivial non finite set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

T is SimplicialComplexStr of the carrier of (TOP-REAL n)

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

{} (TOP-REAL n) is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() open closed compact ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() affinely-independent bounded_below bounded_above real-bounded interval subset-closed with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)

{({} (TOP-REAL n))} is non empty trivial functional finite finite-membered 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered affinely-independent left_end right_end bounded_below bounded_above real-bounded V365( the carrier of (TOP-REAL n)) Element of bool (bool the carrier of (TOP-REAL n))

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

Complex_of {({} (TOP-REAL n))} is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total total affinely-independent simplex-join-closed SimplicialComplexStr of the carrier of (TOP-REAL n)

subset-closed_closure_of {({} (TOP-REAL n))} is non empty finite-membered non with_non-empty_elements subset-closed Element of bool (bool the carrier of (TOP-REAL n))

TopStruct(# the carrier of (TOP-REAL n),(subset-closed_closure_of {({} (TOP-REAL n))}) #) is non empty strict TopStruct

I is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total affinely-independent simplex-join-closed SimplicialComplexStr of the carrier of (TOP-REAL n)

T is SimplicialComplexStr of the carrier of (TOP-REAL n)

n is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

TOP-REAL n is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()

[#] (TOP-REAL n) is non empty non proper non proper open open closed closed convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)

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

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

Euclid n is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct

REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL

n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

Pitag_dist n is non empty Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL n),(REAL n):],REAL:]

[:(REAL n),(REAL n):] is non empty Relation-like set

[:[:(REAL n),(REAL n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set

bool [:[:(REAL n),(REAL n):],REAL:] is non empty non trivial non finite set

MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct

[#] (Euclid n) is non empty non proper Element of bool the carrier of (Euclid n)

the carrier of (Euclid n) is non empty set

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

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

bool (bool 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 V426() TopStruct

TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct

Family_open_set (Euclid n) is Element of bool (bool the carrier of (Euclid n))

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

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

n is set

{n} is non empty trivial finite 1 -element set

T is set

I is set

n is non empty V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of n is non empty set

bool the carrier of n is non empty set

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

BOOL the carrier of n is set

center_of_mass n is Relation-like BOOL the carrier of n -defined the carrier of n -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of n), the carrier of n:]

[:(BOOL the carrier of n), the carrier of n:] is Relation-like set

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

T is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of n

BCS T is non void subset-closed finite-membered non with_non-empty_elements SubdivisionStr of T

the carrier of (BCS T) is set

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

I is open Element of bool the carrier of (BCS T)

E is c=-linear finite finite-membered V365( the carrier of n) Element of bool (bool the carrier of n)

(center_of_mass n) .: E is finite Element of bool the carrier of n

union E is finite Element of bool the carrier of n

{(union E)} is non empty trivial finite finite-membered 1 -element V365( the carrier of n) Element of bool (bool the carrier of n)

Complex_of {(union E)} is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total SimplicialComplexStr of the carrier of n

subset-closed_closure_of {(union E)} is non empty finite-membered non with_non-empty_elements subset-closed Element of bool (bool the carrier of n)

TopStruct(# the carrier of n,(subset-closed_closure_of {(union E)}) #) is non empty strict TopStruct

BCS (Complex_of {(union E)}) is non void subset-closed finite-membered non with_non-empty_elements SubdivisionStr of Complex_of {(union E)}

Vertices (BCS (Complex_of {(union E)})) is Element of bool the carrier of (BCS (Complex_of {(union E)}))

the carrier of (BCS (Complex_of {(union E)})) is set

bool the carrier of (BCS (Complex_of {(union E)})) is non empty set

card (union E) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of omega

(card (union E)) - 1 is real integer finite V55() ext-real Element of REAL

K163((card (union E)),K165(1)) is real integer finite V55() ext-real set

((card (union E)) - 1) / (card (union E)) is real V55() ext-real Element of COMPLEX

K166((card (union E))) is real V55() ext-real non negative set

K164(((card (union E)) - 1),K166((card (union E)))) is real V55() ext-real set

C is Element of the carrier of n

n1 is Element of the carrier of n

C - n1 is Element of the carrier of n

- n1 is Element of the carrier of n

K323(n,C,(- n1)) is Element of the carrier of n

dom (center_of_mass n) is Element of bool (BOOL the carrier of n)

bool (BOOL the carrier of n) is non empty set

c is set

(center_of_mass n) . c is set

TRC is set

(center_of_mass n) . TRC is set

R is Element of the carrier of n

G is Element of the carrier of n

R - G is Element of the carrier of n

- G is Element of the carrier of n

K323(n,R,(- G)) is Element of the carrier of n

the topology of (Complex_of {(union E)}) is finite finite-membered V365( the carrier of (Complex_of {(union E)})) open Element of bool (bool the carrier of (Complex_of {(union E)}))

the carrier of (Complex_of {(union E)}) is set

bool the carrier of (Complex_of {(union E)}) is non empty set

bool (bool the carrier of (Complex_of {(union E)})) is non empty set

bool (union E) is non empty finite finite-membered V365( union E) Element of bool (bool (union E))

bool (union E) is non empty finite finite-membered set

bool (bool (union E)) is non empty finite finite-membered set

G0 is set

p is set

(center_of_mass n) . G0 is set

(center_of_mass n) . p is set

h is non empty finite Element of bool the carrier of n

h is non empty finite Element of bool the carrier of n

h \ h is finite Element of bool the carrier of n

{h} is non empty trivial finite finite-membered 1 -element V365( the carrier of n) Element of bool (bool the carrier of n)

{(h \ h)} is non empty trivial finite finite-membered 1 -element V365( the carrier of n) Element of bool (bool the carrier of n)

cgx is Element of bool (bool the carrier of (Complex_of {(union E)}))

GX is Element of bool (bool the carrier of (Complex_of {(union E)}))

|.(Complex_of {(union E)}).| is Element of bool the carrier of n

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

[#] (Complex_of {(union E)}) is non proper Element of bool the carrier of (Complex_of {(union E)})

subdivision ((center_of_mass n),(Complex_of {(union E)})) is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements SimplicialComplexStr of the carrier of n

[#] (subdivision ((center_of_mass n),(Complex_of {(union E)}))) is non proper Element of bool the carrier of (subdivision ((center_of_mass n),(Complex_of {(union E)})))

the carrier of (subdivision ((center_of_mass n),(Complex_of {(union E)}))) is set

bool the carrier of (subdivision ((center_of_mass n),(Complex_of {(union E)}))) is non empty set

{R} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of n

I is Element of bool the carrier of (BCS (Complex_of {(union E)}))

(center_of_mass n) .: cgx is Element of bool the carrier of n

Im ((center_of_mass n),h) is set

t is Element of the carrier of (BCS (Complex_of {(union E)}))

x is Element of the carrier of n

i1 is Element of the carrier of n

x - i1 is Element of the carrier of n

- i1 is Element of the carrier of n

K323(n,x,(- i1)) is Element of the carrier of n

y is real V55() ext-real Element of REAL

y * (x - i1) is Element of the carrier of n

the Mult of n is non empty Relation-like [:REAL, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of n:], the carrier of n:]

[:REAL, the carrier of n:] is non empty non trivial Relation-like non finite set

[:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial Relation-like non finite set

bool [:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial non finite set

the Mult of n . (y,(x - i1)) is set

1 - 1 is real integer finite V55() ext-real Element of REAL

K163(1,K165(1)) is real integer finite V55() ext-real set

0. n is V65(n) Element of the carrier of n

the ZeroF of n is Element of the carrier of n

y is non empty finite Element of bool the carrier of n

(center_of_mass n) . y is set

rng (center_of_mass n) is Element of bool the carrier of n

x is Element of the carrier of n

{x} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of n

i1 is Element of bool the carrier of (BCS (Complex_of {(union E)}))

(center_of_mass n) .: GX is Element of bool the carrier of n

Im ((center_of_mass n),y) is set

i2 is Element of the carrier of (BCS (Complex_of {(union E)}))

card h is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of omega

1 / (card h) is real V55() ext-real non negative Element of COMPLEX

K166((card h)) is non empty real V55() ext-real positive non negative set

K164(1,K166((card h))) is real V55() ext-real non negative set

card h is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of omega

1 / (card h) is real V55() ext-real non negative Element of COMPLEX

K166((card h)) is non empty real V55() ext-real positive non negative set

K164(1,K166((card h))) is real V55() ext-real non negative set

card y is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of omega

1 / (card y) is real V55() ext-real non negative Element of COMPLEX

K166((card y)) is non empty real V55() ext-real positive non negative set

K164(1,K166((card y))) is real V55() ext-real non negative set

(card y) / (card h) is real V55() ext-real non negative Element of COMPLEX

K164((card y),K166((card h))) is real V55() ext-real non negative set

R - x is Element of the carrier of n

- x is Element of the carrier of n

K323(n,R,(- x)) is Element of the carrier of n

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

r * (R - x) is Element of the carrier of n

the Mult of n is non empty Relation-like [:REAL, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of n:], the carrier of n:]

[:REAL, the carrier of n:] is non empty non trivial Relation-like non finite set

[:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial Relation-like non finite set

bool [:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial non finite set

the Mult of n . (r,(R - x)) is set

r21 is real V55() ext-real Element of REAL

r * r21 is real V55() ext-real Element of REAL

(card y) * 1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative Element of REAL

(card y) * (card h) is non empty real V55() ext-real positive non negative set

K164((card y),(card h)) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set

((card y) * 1) / ((card y) * (card h)) is real V55() ext-real non negative Element of COMPLEX

K166(((card y) * (card h))) is non empty real V55() ext-real positive non negative set

K164(((card y) * 1),K166(((card y) * (card h)))) is real V55() ext-real non negative set

r2 is real V55() ext-real Element of REAL

Sum h is Element of the carrier of n

r1 is real V55() ext-real Element of REAL

r1 * (Sum h) is Element of the carrier of n

the Mult of n . (r1,(Sum h)) is set

r1 * (card h) is real V55() ext-real Element of REAL

ZeroLC n is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of n

h --> r1 is non empty Relation-like h