:: MFOLD_1 semantic presentation

REAL is complex-membered ext-real-membered real-membered V140() non bounded_below non bounded_above V317() set

NAT is ordinal V35() cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V140() bounded_below Element of bool REAL

bool REAL is non empty set

omega is ordinal V35() cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V140() bounded_below set

bool omega is non empty V35() set

bool NAT is non empty V35() set

1 is non empty ordinal natural V11() real ext-real positive non negative V33() V34() V35() cardinal 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 V124() V125() V126() V127() set

RAT is complex-membered ext-real-membered real-membered rational-membered V140() set

INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V140() set

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

[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued V124() V125() V126() V127() set

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

[:[:1,1:],REAL:] is Relation-like V124() V125() V126() set

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

[:REAL,REAL:] is Relation-like V124() V125() V126() set

[:[:REAL,REAL:],REAL:] is Relation-like V124() V125() V126() set

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

2 is non empty ordinal natural V11() real ext-real positive non negative V33() V34() V35() cardinal 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

[:2,2:] is non empty Relation-like RAT -valued INT -valued V124() V125() V126() V127() set

[:[:2,2:],REAL:] is Relation-like V124() V125() V126() set

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

COMPLEX is complex-membered V140() set

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

TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() first-countable L15()

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

K405() is real-membered TopStruct

the carrier of K405() is complex-membered ext-real-membered real-membered set

RealSpace is strict real-membered MetrStruct

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

K412() is TopSpace-like real-membered SubSpace of R^1

K390(K412(),K412()) is strict TopSpace-like TopStruct

the carrier of K390(K412(),K412()) is set

K414() is non empty strict TopSpace-like real-membered V191() SubSpace of R^1

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

bool the carrier of K414() is non empty set

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

K423(2) is TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL 2

the carrier of K423(2) is set

[: the carrier of K414(), the carrier of K423(2):] is Relation-like set

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

K427() is Relation-like the carrier of K414() -defined the carrier of K423(2) -valued Function-like quasi_total Element of bool [: the carrier of K414(), the carrier of K423(2):]

K424() is Element of the carrier of K423(2)

K426(K424()) is strict TopSpace-like T_0 T_1 T_2 SubSpace of K423(2)

the carrier of K426(K424()) is set

0 is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V33() V34() V35() cardinal {} -element V43() V44() V45() V124() V125() V126() V127() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V140() bounded_below bounded_above real-bounded V317() Element of NAT

{} is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V35() cardinal {} -element V43() V44() V45() V124() V125() V126() V127() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V140() bounded_below bounded_above real-bounded V317() set

K328(0,1) is complex-membered ext-real-membered real-membered non left_end non right_end V317() Element of bool REAL

K420(K328(0,1)) is complex-membered ext-real-membered real-membered Element of bool the carrier of K414()

K414() | K420(K328(0,1)) is strict TopSpace-like real-membered SubSpace of K414()

the carrier of (K414() | K420(K328(0,1))) is complex-membered ext-real-membered real-membered set

[: the carrier of K426(K424()), the carrier of (K414() | K420(K328(0,1))):] is Relation-like V124() V125() V126() set

bool [: the carrier of K426(K424()), the carrier of (K414() | K420(K328(0,1))):] is non empty set

K425() is Element of the carrier of K423(2)

K426(K425()) is strict TopSpace-like T_0 T_1 T_2 SubSpace of K423(2)

the carrier of K426(K425()) is set

1 / 2 is non empty V11() real ext-real positive non negative Element of REAL

2 " is non empty V11() real ext-real positive non negative set

1 * (2 ") is non empty V11() real ext-real positive non negative set

3 is non empty ordinal natural V11() real ext-real positive non negative V33() V34() V35() cardinal 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

3 / 2 is non empty V11() real ext-real positive non negative Element of REAL

3 * (2 ") is non empty V11() real ext-real positive non negative set

K328((1 / 2),(3 / 2)) is complex-membered ext-real-membered real-membered non left_end non right_end V317() Element of bool REAL

K420(K328((1 / 2),(3 / 2))) is complex-membered ext-real-membered real-membered Element of bool the carrier of K414()

K414() | K420(K328((1 / 2),(3 / 2))) is strict TopSpace-like real-membered SubSpace of K414()

the carrier of (K414() | K420(K328((1 / 2),(3 / 2)))) is complex-membered ext-real-membered real-membered set

[: the carrier of K426(K425()), the carrier of (K414() | K420(K328((1 / 2),(3 / 2)))):] is Relation-like V124() V125() V126() set

bool [: the carrier of K426(K425()), the carrier of (K414() | K420(K328((1 / 2),(3 / 2)))):] is non empty set

[:COMPLEX,COMPLEX:] is Relation-like V124() set

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

[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like V124() set

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

[:RAT,RAT:] is Relation-like RAT -valued V124() V125() V126() set

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

[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued V124() V125() V126() set

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

[:INT,INT:] is Relation-like RAT -valued INT -valued V124() V125() V126() set

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

[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued V124() V125() V126() set

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

[:NAT,NAT:] is Relation-like RAT -valued INT -valued V124() V125() V126() V127() set

[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V124() V125() V126() V127() set

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

[:COMPLEX,REAL:] is Relation-like V124() V125() V126() set

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

REAL 0 is non empty functional V45() M11( REAL )

TOP-REAL 0 is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() first-countable L15()

0. (TOP-REAL 0) is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V35() cardinal 0 -element V43() V44() V45() V54( TOP-REAL 0) V124() V125() V126() V127() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V140() bounded_below bounded_above real-bounded V317() Element of the carrier of (TOP-REAL 0)

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

the ZeroF of (TOP-REAL 0) is empty ordinal natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V35() cardinal 0 -element V43() V44() V45() V124() V125() V126() V127() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V140() bounded_below bounded_above real-bounded V317() Element of the carrier of (TOP-REAL 0)

{(0. (TOP-REAL 0))} is non empty trivial functional 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set

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

sqrt 1 is V11() real ext-real Element of REAL

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

bool the carrier of R^1 is non empty set

T is set

c

[T,c

{T,c

{T} is non empty trivial 1 -element set

{{T,c

{[T,c

X is set

dom {[T,c

X1 is set

{[T,c

{[T,c

T is non empty TopSpace-like TopStruct

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

the carrier of T is non empty set

bool the carrier of T is non empty set

T | ([#] T) is non empty strict TopSpace-like SubSpace of T

id T is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like V26( the carrier of T) quasi_total continuous Element of bool [: the carrier of T, the carrier of T:]

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

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

K66( the carrier of T) is non empty Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]

dom (id T) is non empty Element of bool the carrier of T

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

the carrier of (T | ([#] T)) is non empty set

bool the carrier of (T | ([#] T)) is non empty set

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

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

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

the carrier of TopStruct(# the carrier of T, the topology of T #) is non empty set

rng (id T) is non empty Element of bool the carrier of T

[: the carrier of T, the carrier of (T | ([#] T)):] is non empty Relation-like set

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

M is non empty Relation-like the carrier of T -defined the carrier of (T | ([#] T)) -valued Function-like V26( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of (T | ([#] T)):]

M " is non empty Relation-like the carrier of (T | ([#] T)) -defined the carrier of T -valued Function-like V26( the carrier of (T | ([#] T))) quasi_total Element of bool [: the carrier of (T | ([#] T)), the carrier of T:]

[: the carrier of (T | ([#] T)), the carrier of T:] is non empty Relation-like set

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

X is Element of bool the carrier of T

(M ") " X is Element of bool the carrier of (T | ([#] T))

([#] T) \ X is Element of bool the carrier of T

X1 is set

M .: X is Element of bool the carrier of (T | ([#] T))

p is set

[p,X1] is set

{p,X1} is non empty set

{p} is non empty trivial 1 -element set

{{p,X1},{p}} is non empty set

[X1,X1] is set

{X1,X1} is non empty set

{X1} is non empty trivial 1 -element set

{{X1,X1},{X1}} is non empty set

([#] (T | ([#] T))) \ ((M ") " X) is Element of bool the carrier of (T | ([#] T))

([#] T) /\ ([#] T) is open closed Element of bool the carrier of T

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

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

the topology of (T | ([#] T)) is non empty open Element of bool (bool the carrier of (T | ([#] T)))

bool (bool the carrier of (T | ([#] T))) is non empty set

T is ordinal natural V11() real ext-real non negative V35() cardinal set

TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

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

c

the carrier of c

[: the carrier of c

bool [: the carrier of c

[: the carrier of c

bool [: the carrier of c

M is non empty Relation-like the carrier of c

X is Element of the carrier of c

M . X is V11() real ext-real set

M . X is V11() real ext-real Element of the carrier of R^1

[#] c

bool the carrier of c

[#] (TOP-REAL T) is non empty non proper functional open closed dense non boundary Element of bool the carrier of (TOP-REAL T)

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

p is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

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

X1 * p is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

U1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

S1 is V11() real ext-real set

S1 * U1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

X is non empty Relation-like the carrier of c

X is non empty Relation-like the carrier of c

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

bool the carrier of c

X1 is Element of the carrier of c

X . X1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

p is functional Element of bool the carrier of (TOP-REAL T)

Euclid T is non empty strict Reflexive discerning V83() triangle MetrStruct

the carrier of (Euclid T) is non empty set

[#] c

[#] (TOP-REAL T) is non empty non proper functional open closed dense non boundary Element of bool the carrier of (TOP-REAL T)

p1 is ordinal natural V11() real ext-real non negative V33() V34() V35() cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

TOP-REAL p1 is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() first-countable L15()

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

M . X1 is V11() real ext-real Element of the carrier of R^1

Int p is functional open Element of bool the carrier of (TOP-REAL T)

U1 is Element of the carrier of (Euclid T)

S2 is V11() real ext-real set

Ball (U1,S2) is Element of bool the carrier of (Euclid T)

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

U2 is V11() real ext-real set

S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

S2 / 2 is V11() real ext-real Element of REAL

S2 * (2 ") is V11() real ext-real set

Ball (S1,(S2 / 2)) is functional open V162( TOP-REAL p1) Element of bool the carrier of (TOP-REAL p1)

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

{ b

(Ball (S1,(S2 / 2))) /\ ([#] c

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

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

X2 is Element of bool the carrier of c

the topology of c

bool (bool the carrier of c

{ |.b

|.S1.| is V11() real ext-real non negative Element of REAL

f is set

U is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.U.| is V11() real ext-real non negative Element of REAL

f is non empty complex-membered ext-real-membered real-membered set

|.S1.| + (S2 / 2) is V11() real ext-real Element of REAL

U is ext-real set

U3 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.U3.| is V11() real ext-real non negative Element of REAL

U3 - S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

- S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),U3,(- S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

the U7 of (TOP-REAL p1) is non empty Relation-like [: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] -defined the carrier of (TOP-REAL p1) -valued Function-like V26([: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):]) quasi_total Element of bool [:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):]

[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] is non empty Relation-like set

[:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):] is non empty Relation-like set

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

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),U3,(- S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(U3 - S1).| is V11() real ext-real non negative Element of REAL

|.(- S1).| is V11() real ext-real non negative Element of REAL

|.U3.| - |.(- S1).| is V11() real ext-real Element of REAL

- |.(- S1).| is V11() real ext-real non positive set

|.U3.| + (- |.(- S1).|) is V11() real ext-real set

U3 + (- S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(U3 + (- S1)).| is V11() real ext-real non negative Element of REAL

|.U3.| - |.S1.| is V11() real ext-real Element of REAL

- |.S1.| is V11() real ext-real non positive set

|.U3.| + (- |.S1.|) is V11() real ext-real set

(|.U3.| - |.S1.|) + |.S1.| is V11() real ext-real Element of REAL

(S2 / 2) + |.S1.| is V11() real ext-real Element of REAL

sup f is ext-real set

U is V11() real ext-real set

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

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

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

T2 is Element of bool the carrier of c

M .: T2 is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1

T2 /\ X2 is Element of bool the carrier of c

f2 is Element of bool the carrier of c

X .: f2 is functional Element of bool the carrier of (TOP-REAL T)

S is set

dom X is non empty Element of bool the carrier of c

Q is set

X . Q is Relation-like Function-like set

S is Element of the carrier of c

M . S is V11() real ext-real Element of the carrier of R^1

U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U5 is V11() real ext-real set

U5 * U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

y is Element of the carrier of (Euclid T)

q is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U2 * S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U5 - U2 is V11() real ext-real set

- U2 is V11() real ext-real set

U5 + (- U2) is V11() real ext-real set

abs (U5 - U2) is V11() real ext-real non negative Element of REAL

|.U4.| is V11() real ext-real non negative Element of REAL

(abs (U5 - U2)) * |.U4.| is V11() real ext-real non negative Element of REAL

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

abs r2 is V11() real ext-real non negative Element of REAL

(abs r2) * |.U4.| is V11() real ext-real non negative Element of REAL

(U5 - U2) * U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.((U5 - U2) * U4).| is V11() real ext-real non negative Element of REAL

0. (TOP-REAL p1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V54( TOP-REAL p1) V124() V125() V126() Element of the carrier of (TOP-REAL p1)

the ZeroF of (TOP-REAL p1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

gqq is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

- q is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

gqq + (- q) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

the U7 of (TOP-REAL p1) is non empty Relation-like [: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] -defined the carrier of (TOP-REAL p1) -valued Function-like V26([: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):]) quasi_total Element of bool [:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):]

[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] is non empty Relation-like set

[:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):] is non empty Relation-like set

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

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),gqq,(- q)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(gqq + (- q)).| is V11() real ext-real non negative Element of REAL

|.gqq.| is V11() real ext-real non negative Element of REAL

|.(- q).| is V11() real ext-real non negative Element of REAL

|.gqq.| + |.(- q).| is V11() real ext-real non negative Element of REAL

|.(0. (TOP-REAL p1)).| is V11() real ext-real non negative Element of REAL

|.gqq.| + |.(0. (TOP-REAL p1)).| is V11() real ext-real non negative Element of REAL

|.gqq.| + {} is V11() real ext-real non negative Element of REAL

gqq - q is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),gqq,(- q)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(gqq - q).| is V11() real ext-real non negative Element of REAL

Ball (q,S2) is functional open V162( TOP-REAL p1) Element of bool the carrier of (TOP-REAL p1)

{ b

S2 / U is V11() real ext-real Element of COMPLEX

U " is V11() real ext-real set

S2 * (U ") is V11() real ext-real set

U2 - (S2 / U) is V11() real ext-real set

- (S2 / U) is V11() real ext-real set

U2 + (- (S2 / U)) is V11() real ext-real set

U2 + (S2 / U) is V11() real ext-real set

].(U2 - (S2 / U)),(U2 + (S2 / U)).[ is non left_end non right_end V317() set

(S2 / U) + U2 is V11() real ext-real set

{} + U2 is V11() real ext-real set

- (S2 / U) is V11() real ext-real Element of COMPLEX

(- (S2 / U)) + U2 is V11() real ext-real set

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

T2 is Element of bool the carrier of c

M .: T2 is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1

T2 /\ X2 is Element of bool the carrier of c

f2 is Element of bool the carrier of c

X .: f2 is functional Element of bool the carrier of (TOP-REAL T)

S is set

dom X is non empty Element of bool the carrier of c

Q is set

X . Q is Relation-like Function-like set

S is Element of the carrier of c

M . S is V11() real ext-real Element of the carrier of R^1

U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U5 is V11() real ext-real set

U5 * U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

y is Element of the carrier of (Euclid T)

q is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U2 * S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

abs U5 is V11() real ext-real non negative Element of REAL

|.U4.| is V11() real ext-real non negative Element of REAL

(abs U5) * |.U4.| is V11() real ext-real non negative Element of REAL

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

abs r2 is V11() real ext-real non negative Element of REAL

(abs r2) * |.U4.| is V11() real ext-real non negative Element of REAL

|.(U5 * U4).| is V11() real ext-real non negative Element of REAL

dom M is non empty Element of bool the carrier of c

U5 - U2 is V11() real ext-real set

- U2 is V11() real ext-real set

U5 + (- U2) is V11() real ext-real set

abs (U5 - U2) is V11() real ext-real non negative Element of REAL

(S2 / U) * U is V11() real ext-real set

(abs U5) * U is V11() real ext-real Element of REAL

U / U is V11() real ext-real Element of COMPLEX

U * (U ") is V11() real ext-real set

S2 / (U / U) is V11() real ext-real Element of COMPLEX

(U / U) " is V11() real ext-real set

S2 * ((U / U) ") is V11() real ext-real set

S2 / 1 is V11() real ext-real Element of REAL

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

S2 * (1 ") is V11() real ext-real set

|.U4.| * (abs U5) is V11() real ext-real non negative Element of REAL

U * (abs U5) is V11() real ext-real Element of REAL

0. (TOP-REAL p1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V54( TOP-REAL p1) V124() V125() V126() Element of the carrier of (TOP-REAL p1)

the ZeroF of (TOP-REAL p1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

gqq is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.gqq.| is V11() real ext-real non negative Element of REAL

- q is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

gqq + (- q) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

the U7 of (TOP-REAL p1) is non empty Relation-like [: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] -defined the carrier of (TOP-REAL p1) -valued Function-like V26([: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):]) quasi_total Element of bool [:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):]

[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] is non empty Relation-like set

[:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):] is non empty Relation-like set

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

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),gqq,(- q)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(gqq + (- q)).| is V11() real ext-real non negative Element of REAL

|.(- q).| is V11() real ext-real non negative Element of REAL

|.gqq.| + |.(- q).| is V11() real ext-real non negative Element of REAL

|.(0. (TOP-REAL p1)).| is V11() real ext-real non negative Element of REAL

|.gqq.| + |.(0. (TOP-REAL p1)).| is V11() real ext-real non negative Element of REAL

|.gqq.| + {} is V11() real ext-real non negative Element of REAL

gqq - q is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),gqq,(- q)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(gqq - q).| is V11() real ext-real non negative Element of REAL

Ball (q,S2) is functional open V162( TOP-REAL p1) Element of bool the carrier of (TOP-REAL p1)

{ b

U2 is V11() real ext-real set

S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

S2 / 2 is V11() real ext-real Element of REAL

S2 * (2 ") is V11() real ext-real set

abs U2 is V11() real ext-real non negative Element of REAL

(S2 / 2) / (abs U2) is V11() real ext-real Element of REAL

(abs U2) " is V11() real ext-real non negative set

(S2 / 2) * ((abs U2) ") is V11() real ext-real set

Ball (S1,((S2 / 2) / (abs U2))) is functional open V162( TOP-REAL p1) Element of bool the carrier of (TOP-REAL p1)

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

{ b

(Ball (S1,((S2 / 2) / (abs U2)))) /\ ([#] c

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

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

X2 is Element of bool the carrier of c

the topology of c

bool (bool the carrier of c

{ |.b

|.S1.| is V11() real ext-real non negative Element of REAL

f is set

U is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.U.| is V11() real ext-real non negative Element of REAL

f is non empty complex-membered ext-real-membered real-membered set

|.S1.| + ((S2 / 2) / (abs U2)) is V11() real ext-real Element of REAL

U is ext-real set

U3 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.U3.| is V11() real ext-real non negative Element of REAL

U3 - S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

- S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),U3,(- S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

the U7 of (TOP-REAL p1) is non empty Relation-like [: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] -defined the carrier of (TOP-REAL p1) -valued Function-like V26([: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):]) quasi_total Element of bool [:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):]

[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] is non empty Relation-like set

[:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):] is non empty Relation-like set

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

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),U3,(- S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(U3 - S1).| is V11() real ext-real non negative Element of REAL

|.(- S1).| is V11() real ext-real non negative Element of REAL

|.U3.| - |.(- S1).| is V11() real ext-real Element of REAL

- |.(- S1).| is V11() real ext-real non positive set

|.U3.| + (- |.(- S1).|) is V11() real ext-real set

U3 + (- S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(U3 + (- S1)).| is V11() real ext-real non negative Element of REAL

|.U3.| - |.S1.| is V11() real ext-real Element of REAL

- |.S1.| is V11() real ext-real non positive set

|.U3.| + (- |.S1.|) is V11() real ext-real set

(|.U3.| - |.S1.|) + |.S1.| is V11() real ext-real Element of REAL

((S2 / 2) / (abs U2)) + |.S1.| is V11() real ext-real Element of REAL

sup f is ext-real set

U is V11() real ext-real set

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

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

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

T2 is Element of bool the carrier of c

M .: T2 is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1

T2 /\ X2 is Element of bool the carrier of c

f2 is Element of bool the carrier of c

X .: f2 is functional Element of bool the carrier of (TOP-REAL T)

S is set

dom X is non empty Element of bool the carrier of c

Q is set

X . Q is Relation-like Function-like set

S is Element of the carrier of c

M . S is V11() real ext-real Element of the carrier of R^1

U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U5 is V11() real ext-real set

U5 * U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

y is Element of the carrier of (Euclid T)

q is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U2 * S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U5 - U2 is V11() real ext-real set

- U2 is V11() real ext-real set

U5 + (- U2) is V11() real ext-real set

abs (U5 - U2) is V11() real ext-real non negative Element of REAL

|.U4.| is V11() real ext-real non negative Element of REAL

(abs (U5 - U2)) * |.U4.| is V11() real ext-real non negative Element of REAL

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

abs r2 is V11() real ext-real non negative Element of REAL

(abs r2) * |.U4.| is V11() real ext-real non negative Element of REAL

(U5 - U2) * U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.((U5 - U2) * U4).| is V11() real ext-real non negative Element of REAL

U4 - S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

- S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),U4,(- S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

the U7 of (TOP-REAL p1) is non empty Relation-like [: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] -defined the carrier of (TOP-REAL p1) -valued Function-like V26([: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):]) quasi_total Element of bool [:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):]

[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] is non empty Relation-like set

[:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):] is non empty Relation-like set

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

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),U4,(- S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(U4 - S1).| is V11() real ext-real non negative Element of REAL

(abs U2) * |.(U4 - S1).| is V11() real ext-real non negative Element of REAL

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

abs r3 is V11() real ext-real non negative Element of REAL

(abs r3) * |.(U4 - S1).| is V11() real ext-real non negative Element of REAL

U2 * (U4 - S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(U2 * (U4 - S1)).| is V11() real ext-real non negative Element of REAL

(abs U2) * ((S2 / 2) / (abs U2)) is V11() real ext-real Element of REAL

(abs U2) / (abs U2) is V11() real ext-real non negative Element of REAL

(abs U2) * ((abs U2) ") is V11() real ext-real non negative set

(S2 / 2) / ((abs U2) / (abs U2)) is V11() real ext-real Element of REAL

((abs U2) / (abs U2)) " is V11() real ext-real non negative set

(S2 / 2) * (((abs U2) / (abs U2)) ") is V11() real ext-real set

(S2 / 2) / 1 is V11() real ext-real Element of REAL

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

(S2 / 2) * (1 ") is V11() real ext-real set

(S2 / 2) + (S2 / 2) is V11() real ext-real Element of REAL

|.((U5 - U2) * U4).| + |.(U2 * (U4 - S1)).| is V11() real ext-real non negative Element of REAL

((U5 - U2) * U4) + (U2 * (U4 - S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),((U5 - U2) * U4),(U2 * (U4 - S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(((U5 - U2) * U4) + (U2 * (U4 - S1))).| is V11() real ext-real non negative Element of REAL

U2 * U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

(U5 * U4) - (U2 * U4) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

- (U2 * U4) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),(U5 * U4),(- (U2 * U4))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),(U5 * U4),(- (U2 * U4))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

((U5 * U4) - (U2 * U4)) + (U2 * (U4 - S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),((U5 * U4) - (U2 * U4)),(U2 * (U4 - S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

(U2 * U4) - (U2 * S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

- (U2 * S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),(U2 * U4),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),(U2 * U4),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

((U5 * U4) - (U2 * U4)) + ((U2 * U4) - (U2 * S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),((U5 * U4) - (U2 * U4)),((U2 * U4) - (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

((U5 * U4) - (U2 * U4)) + (U2 * U4) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),((U5 * U4) - (U2 * U4)),(U2 * U4)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

(((U5 * U4) - (U2 * U4)) + (U2 * U4)) - (U2 * S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),(((U5 * U4) - (U2 * U4)) + (U2 * U4)),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),(((U5 * U4) - (U2 * U4)) + (U2 * U4)),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

(U5 * U4) - (U2 * S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),(U5 * U4),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),(U5 * U4),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

gqq is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

Ball (q,S2) is functional open V162( TOP-REAL p1) Element of bool the carrier of (TOP-REAL p1)

{ b

(S2 / 2) / U is V11() real ext-real Element of REAL

U " is V11() real ext-real set

(S2 / 2) * (U ") is V11() real ext-real set

U2 - ((S2 / 2) / U) is V11() real ext-real Element of REAL

- ((S2 / 2) / U) is V11() real ext-real set

U2 + (- ((S2 / 2) / U)) is V11() real ext-real set

U2 + ((S2 / 2) / U) is V11() real ext-real Element of REAL

].(U2 - ((S2 / 2) / U)),(U2 + ((S2 / 2) / U)).[ is non left_end non right_end V317() set

((S2 / 2) / U) + U2 is V11() real ext-real Element of REAL

{} + U2 is V11() real ext-real set

- ((S2 / 2) / U) is V11() real ext-real Element of REAL

(- ((S2 / 2) / U)) + U2 is V11() real ext-real Element of REAL

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

T2 is Element of bool the carrier of c

M .: T2 is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1

T2 /\ X2 is Element of bool the carrier of c

f2 is Element of bool the carrier of c

X .: f2 is functional Element of bool the carrier of (TOP-REAL T)

S is set

dom X is non empty Element of bool the carrier of c

Q is set

X . Q is Relation-like Function-like set

S is Element of the carrier of c

M . S is V11() real ext-real Element of the carrier of R^1

U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U5 is V11() real ext-real set

U5 * U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

y is Element of the carrier of (Euclid T)

q is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U2 * S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

U5 - U2 is V11() real ext-real set

- U2 is V11() real ext-real set

U5 + (- U2) is V11() real ext-real set

abs (U5 - U2) is V11() real ext-real non negative Element of REAL

|.U4.| is V11() real ext-real non negative Element of REAL

(abs (U5 - U2)) * |.U4.| is V11() real ext-real non negative Element of REAL

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

abs r2 is V11() real ext-real non negative Element of REAL

(abs r2) * |.U4.| is V11() real ext-real non negative Element of REAL

(U5 - U2) * U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.((U5 - U2) * U4).| is V11() real ext-real non negative Element of REAL

dom M is non empty Element of bool the carrier of c

((S2 / 2) / U) * U is V11() real ext-real Element of REAL

(abs (U5 - U2)) * U is V11() real ext-real Element of REAL

U / U is V11() real ext-real Element of COMPLEX

U * (U ") is V11() real ext-real set

(S2 / 2) / (U / U) is V11() real ext-real Element of REAL

(U / U) " is V11() real ext-real set

(S2 / 2) * ((U / U) ") is V11() real ext-real set

(S2 / 2) / 1 is V11() real ext-real Element of REAL

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

(S2 / 2) * (1 ") is V11() real ext-real set

|.U4.| * (abs (U5 - U2)) is V11() real ext-real non negative Element of REAL

U * (abs (U5 - U2)) is V11() real ext-real Element of REAL

U4 - S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

- S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),U4,(- S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

the U7 of (TOP-REAL p1) is non empty Relation-like [: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] -defined the carrier of (TOP-REAL p1) -valued Function-like V26([: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):]) quasi_total Element of bool [:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):]

[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):] is non empty Relation-like set

[:[: the carrier of (TOP-REAL p1), the carrier of (TOP-REAL p1):], the carrier of (TOP-REAL p1):] is non empty Relation-like set

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

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),U4,(- S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(U4 - S1).| is V11() real ext-real non negative Element of REAL

(abs U2) * |.(U4 - S1).| is V11() real ext-real non negative Element of REAL

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

abs r3 is V11() real ext-real non negative Element of REAL

(abs r3) * |.(U4 - S1).| is V11() real ext-real non negative Element of REAL

U2 * (U4 - S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(U2 * (U4 - S1)).| is V11() real ext-real non negative Element of REAL

(abs U2) * ((S2 / 2) / (abs U2)) is V11() real ext-real Element of REAL

(abs U2) / (abs U2) is V11() real ext-real non negative Element of REAL

(abs U2) * ((abs U2) ") is V11() real ext-real non negative set

(S2 / 2) / ((abs U2) / (abs U2)) is V11() real ext-real Element of REAL

((abs U2) / (abs U2)) " is V11() real ext-real non negative set

(S2 / 2) * (((abs U2) / (abs U2)) ") is V11() real ext-real set

(S2 / 2) + (S2 / 2) is V11() real ext-real Element of REAL

|.((U5 - U2) * U4).| + |.(U2 * (U4 - S1)).| is V11() real ext-real non negative Element of REAL

((U5 - U2) * U4) + (U2 * (U4 - S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),((U5 - U2) * U4),(U2 * (U4 - S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

|.(((U5 - U2) * U4) + (U2 * (U4 - S1))).| is V11() real ext-real non negative Element of REAL

U2 * U4 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

(U5 * U4) - (U2 * U4) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

- (U2 * U4) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),(U5 * U4),(- (U2 * U4))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),(U5 * U4),(- (U2 * U4))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

((U5 * U4) - (U2 * U4)) + (U2 * (U4 - S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),((U5 * U4) - (U2 * U4)),(U2 * (U4 - S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

(U2 * U4) - (U2 * S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

- (U2 * S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),(U2 * U4),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),(U2 * U4),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

((U5 * U4) - (U2 * U4)) + ((U2 * U4) - (U2 * S1)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),((U5 * U4) - (U2 * U4)),((U2 * U4) - (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

((U5 * U4) - (U2 * U4)) + (U2 * U4) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),((U5 * U4) - (U2 * U4)),(U2 * U4)) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

(((U5 * U4) - (U2 * U4)) + (U2 * U4)) - (U2 * S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),(((U5 * U4) - (U2 * U4)) + (U2 * U4)),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),(((U5 * U4) - (U2 * U4)) + (U2 * U4)),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

(U5 * U4) - (U2 * S1) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K184((TOP-REAL p1),(U5 * U4),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

K155( the carrier of (TOP-REAL p1), the U7 of (TOP-REAL p1),(U5 * U4),(- (U2 * S1))) is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

gqq is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

Ball (q,S2) is functional open V162( TOP-REAL p1) Element of bool the carrier of (TOP-REAL p1)

{ b

U2 is V11() real ext-real set

X1 is Element of the carrier of c

p is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

M . X1 is V11() real ext-real Element of the carrier of R^1

p1 is V11() real ext-real set

X . p is Relation-like Function-like set

p1 * p is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

T is ordinal natural V11() real ext-real non negative V35() cardinal set

TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

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

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

T is ordinal natural V11() real ext-real non negative V35() cardinal set

TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

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

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

the Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T) is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

the V11() real ext-real set is V11() real ext-real set

Ball ( the Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T), the V11() real ext-real set ) is functional open Element of bool the carrier of (TOP-REAL T)

{ b

c

M is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

X is V11() real ext-real set

Ball (M,X) is functional open Element of bool the carrier of (TOP-REAL T)

{ b

T is ordinal natural V11() real ext-real non negative V35() cardinal set

TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

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

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

0. (TOP-REAL T) is Relation-like NAT -defined Function-like V35() T -element V43() V44() V54( TOP-REAL T) V124() V125() V126() Element of the carrier of (TOP-REAL T)

the ZeroF of (TOP-REAL T) is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

Ball ((0. (TOP-REAL T)),1) is non empty functional open Element of bool the carrier of (TOP-REAL T)

{ b

c

T is ordinal natural V11() real ext-real non negative V35() cardinal set

TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

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

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

c

M is functional open Element of bool the carrier of (TOP-REAL T)

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

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

TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #) is non empty strict TopSpace-like V204() second-countable TopStruct

Euclid T is non empty strict Reflexive discerning V83() triangle MetrStruct

TopSpaceMetr (Euclid T) is metrizable first-countable TopStruct

the carrier of (Euclid T) is non empty set

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

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

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

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

X is Element of the carrier of (Euclid T)

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

Ball (X,X1) is Element of bool the carrier of (Euclid T)

p is non empty V11() real ext-real positive non negative set

Ball (c

{ b

U1 is functional open (T) Element of bool the carrier of (TOP-REAL T)

p1 is ordinal natural V11() real ext-real non negative V33() V34() V35() cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

TOP-REAL p1 is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() first-countable L15()

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

Ball (X,p) is Element of bool the carrier of (Euclid T)

S1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1)

Ball (S1,p) is non empty functional open V162( TOP-REAL p1) Element of bool the carrier of (TOP-REAL p1)

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

{ b

T is ordinal natural V11() real ext-real non negative V35() cardinal set

TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

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

c

M is V11() real ext-real set

Ball (c

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

{ b

(TOP-REAL T) | (Ball (c

T is ordinal natural V11() real ext-real non negative V35() cardinal set

TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

0. (TOP-REAL T) is Relation-like NAT -defined Function-like V35() T -element V43() V44() V54( TOP-REAL T) V124() V125() V126() Element of the carrier of (TOP-REAL T)

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

the ZeroF of (TOP-REAL T) is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)

(T,(0. (TOP-REAL T)),1) is TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T

Ball ((0. (TOP-REAL T)),1) is non empty functional open Element of bool the carrier of (TOP-REAL T)

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

{ b

(TOP-REAL T) | (Ball ((0. (TOP-REAL T)),1)) is non empty strict TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T

T is ordinal natural V11() real ext-real non negative V35() cardinal set

(T) is TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T

TOP-REAL T is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()

0. (TOP-REAL T) is Relation-like NAT -defined Function-like V35() T -element V43()