:: MFOLD_1 semantic presentation

bool REAL is non empty set

bool omega is non empty V35() set
bool NAT is non empty V35() set

[:1,1:] is non empty Relation-like RAT -valued INT -valued V124() V125() V126() V127() 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

bool is non empty set

[: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

bool 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 () is non empty functional set

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

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

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

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 / 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

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

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

the carrier of () is non empty functional 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
c2 is set
[T,c2] is set
{T,c2} is non empty set
{T} is non empty trivial 1 -element set
{{T,c2},{T}} is non empty set

X is set
dom {[T,c2]} is non empty trivial 1 -element set
X1 is set
{[T,c2]} . X is set
{[T,c2]} . X1 is set
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

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 () is non empty functional set
c2 is non empty TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
the carrier of c2 is non empty set
[: the carrier of c2, the carrier of R^1:] is non empty Relation-like V124() V125() V126() set
bool [: the carrier of c2, the carrier of R^1:] is non empty set
[: the carrier of c2, the carrier of ():] is non empty Relation-like set
bool [: the carrier of c2, the carrier of ():] is non empty set
M is non empty Relation-like the carrier of c2 -defined the carrier of R^1 -valued Function-like V26( the carrier of c2) quasi_total V124() V125() V126() Element of bool [: the carrier of c2, the carrier of R^1:]
X is Element of the carrier of c2
M . X is V11() real ext-real set
M . X is V11() real ext-real Element of the carrier of R^1
[#] c2 is non empty non proper open closed dense non boundary Element of bool the carrier of c2
bool the carrier of c2 is non empty set
[#] () is non empty non proper functional open closed dense non boundary Element of bool the carrier of ()
bool the carrier of () 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 ()
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 ()
U1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()
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 ()
X is non empty Relation-like the carrier of c2 -defined the carrier of () -valued Function-like V26( the carrier of c2) quasi_total Element of bool [: the carrier of c2, the carrier of ():]
X is non empty Relation-like the carrier of c2 -defined the carrier of () -valued Function-like V26( the carrier of c2) quasi_total Element of bool [: the carrier of c2, the carrier of ():]
bool the carrier of () is non empty set
bool the carrier of c2 is non empty set
X1 is Element of the carrier of c2
X . X1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()
p is functional Element of bool the carrier of ()

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

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 ()
U1 is Element of the carrier of ()
S2 is V11() real ext-real set
Ball (U1,S2) is Element of bool the carrier of ()
bool the carrier of () 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
{ b1 where b1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1) : not S2 / 2 <= |.(b1 - S1).| } is set
(Ball (S1,(S2 / 2))) /\ ([#] c2) is Element of bool the carrier of c2
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 c2
the topology of c2 is non empty open Element of bool (bool the carrier of c2)
bool (bool the carrier of c2) is non empty set
{ |.b1.| where b1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of () : b1 in X2 } is set
|.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

|.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

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

T2 is Element of bool the carrier of c2

T2 /\ X2 is Element of bool the carrier of c2
f2 is Element of bool the carrier of c2
X .: f2 is functional Element of bool the carrier of ()
S is set
dom X is non empty Element of bool the carrier of c2
Q is set

S is Element of the carrier of c2
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 ()
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)
{ b1 where b1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1) : not S2 <= |.(b1 - q).| } is set
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

T2 is Element of bool the carrier of c2

T2 /\ X2 is Element of bool the carrier of c2
f2 is Element of bool the carrier of c2
X .: f2 is functional Element of bool the carrier of ()
S is set
dom X is non empty Element of bool the carrier of c2
Q is set

S is Element of the carrier of c2
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 ()
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 c2
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)
{ b1 where b1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1) : not S2 <= |.(b1 - q).| } is 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
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
{ b1 where b1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1) : not (S2 / 2) / (abs U2) <= |.(b1 - S1).| } is set
(Ball (S1,((S2 / 2) / (abs U2)))) /\ ([#] c2) is Element of bool the carrier of c2
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 c2
the topology of c2 is non empty open Element of bool (bool the carrier of c2)
bool (bool the carrier of c2) is non empty set
{ |.b1.| where b1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of () : b1 in X2 } is set
|.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

|.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

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

T2 is Element of bool the carrier of c2

T2 /\ X2 is Element of bool the carrier of c2
f2 is Element of bool the carrier of c2
X .: f2 is functional Element of bool the carrier of ()
S is set
dom X is non empty Element of bool the carrier of c2
Q is set

S is Element of the carrier of c2
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 ()
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)
{ b1 where b1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1) : not S2 <= |.(b1 - q).| } is set
(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

T2 is Element of bool the carrier of c2

T2 /\ X2 is Element of bool the carrier of c2
f2 is Element of bool the carrier of c2
X .: f2 is functional Element of bool the carrier of ()
S is set
dom X is non empty Element of bool the carrier of c2
Q is set

S is Element of the carrier of c2
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 ()
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 c2
((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)
{ b1 where b1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1) : not S2 <= |.(b1 - q).| } is set
U2 is V11() real ext-real set
X1 is Element of the carrier of c2
p is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()
M . X1 is V11() real ext-real Element of the carrier of R^1
p1 is V11() real ext-real 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 is non empty TopSpace-like T_0 T_1 T_2 V100() V146() V147() V148() V149() V150() V151() V152() V158() L15()
the carrier of () is non empty functional set
bool the carrier of () is non empty 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 () is non empty functional set
bool the carrier of () is non empty set
the Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of () is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()
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 (), the V11() real ext-real set ) is functional open Element of bool the carrier of ()
{ b1 where b1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of () : not the V11() real ext-real set <= |.(b1 - the Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()).| } is set
c2 is functional Element of bool the carrier of ()
M is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()
X is V11() real ext-real set
Ball (M,X) is functional open Element of bool the carrier of ()
{ b1 where b1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of () : not X <= |.(b1 - M).| } is 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 () is non empty functional set
bool the carrier of () is non empty set
0. () is Relation-like NAT -defined Function-like V35() T -element V43() V44() V54( TOP-REAL T) V124() V125() V126() Element of the carrier of ()
the ZeroF of () is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()
Ball ((0. ()),1) is non empty functional open Element of bool the carrier of ()
{ b1 where b1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of () : not 1 <= |.(b1 - (0. ())).| } is set
c2 is functional open (T) Element of bool the carrier of ()

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 () is non empty functional set
bool the carrier of () is non empty set
c2 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()
M is functional open Element of bool the carrier of ()
the topology of () is non empty open Element of bool (bool the carrier of ())
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (), the topology of () #) is non empty strict TopSpace-like V204() second-countable TopStruct

the carrier of () is non empty set
Family_open_set () is Element of bool (bool the carrier of ())
bool the carrier of () is non empty set
bool (bool the carrier of ()) is non empty set
TopStruct(# the carrier of (),() #) is non empty strict TopStruct
X is Element of the carrier of ()
X1 is V11() real ext-real Element of REAL
Ball (X,X1) is Element of bool the carrier of ()
p is non empty V11() real ext-real positive non negative set
Ball (c2,p) is non empty functional open Element of bool the carrier of ()
{ b1 where b1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of () : not p <= |.(b1 - c2).| } is set
U1 is functional open (T) Element of bool the carrier of ()

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 ()
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
{ b1 where b1 is Relation-like NAT -defined Function-like V35() p1 -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL p1) : not p <= |.(b1 - S1).| } is 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 () is non empty functional set
c2 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()
M is V11() real ext-real set
Ball (c2,M) is functional open Element of bool the carrier of ()
bool the carrier of () is non empty set
{ b1 where b1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of () : not M <= |.(b1 - c2).| } is set
() | (Ball (c2,M)) is strict 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. () is Relation-like NAT -defined Function-like V35() T -element V43() V44() V54( TOP-REAL T) V124() V125() V126() Element of the carrier of ()
the carrier of () is non empty functional set
the ZeroF of () is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of ()
(T,(0. ()),1) is TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
Ball ((0. ()),1) is non empty functional open Element of bool the carrier of ()
bool the carrier of () is non empty set
{ b1 where b1 is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of () : not 1 <= |.(b1 - (0. ())).| } is set
() | (Ball ((0. ()),1)) is non empty strict 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()