:: 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₂ is set
[T,c₂] is set
{T,c₂} is non empty set
{T} is non empty trivial 1 -element set
{{T,c₂},{T}} is non empty set
{[T,c₂]} is non empty trivial Relation-like Function-like constant 1 -element set
X is set
dom {[T,c₂]} is non empty trivial 1 -element set
X1 is set
{[T,c₂]} . X is set
{[T,c₂]} . 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
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₂ is non empty TopSpace-like T_0 T_1 T_2 SubSpace of TOP-REAL T
the carrier of c₂ is non empty set
[: the carrier of c₂, the carrier of R^1:] is non empty Relation-like V124() V125() V126() set
bool [: the carrier of c₂, the carrier of R^1:] is non empty set
[: the carrier of c₂, the carrier of (TOP-REAL T):] is non empty Relation-like set
bool [: the carrier of c₂, the carrier of (TOP-REAL T):] is non empty set
M is non empty Relation-like the carrier of c₂ -defined the carrier of R^1 -valued Function-like V26( the carrier of c₂) quasi_total V124() V125() V126() Element of bool [: the carrier of c₂, the carrier of R^1:]
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₂ is non empty non proper open closed dense non boundary Element of bool the carrier of c₂
bool the carrier of c₂ is non empty set
[#] (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₂ -defined the carrier of (TOP-REAL T) -valued Function-like V26( the carrier of c₂) quasi_total Element of bool [: the carrier of c₂, the carrier of (TOP-REAL T):]
X is non empty Relation-like the carrier of c₂ -defined the carrier of (TOP-REAL T) -valued Function-like V26( the carrier of c₂) quasi_total Element of bool [: the carrier of c₂, the carrier of (TOP-REAL T):]
bool the carrier of (TOP-REAL T) is non empty set
bool the carrier of c₂ is non empty set
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₂ is non empty non proper open closed dense non boundary Element of 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)
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₁ where b₁ 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 <= |.(b₁ - S1).| } is set
(Ball (S1,(S2 / 2))) /\ ([#] c₂) is Element of bool the carrier of 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₂ is non empty open Element of bool (bool the carrier of c₂)
bool (bool the carrier of c₂) is non empty set
{ |.b₁.| where b₁ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T) : b₁ 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
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₁ where b₁ 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 <= |.(b₁ - 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
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₁ where b₁ 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 <= |.(b₁ - 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
{ b₁ where b₁ 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) <= |.(b₁ - S1).| } is set
(Ball (S1,((S2 / 2) / (abs U2)))) /\ ([#] c₂) is Element of bool the carrier of 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₂ is non empty open Element of bool (bool the carrier of c₂)
bool (bool the carrier of c₂) is non empty set
{ |.b₁.| where b₁ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T) : b₁ 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
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₁ where b₁ 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 <= |.(b₁ - 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
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₁ where b₁ 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 <= |.(b₁ - q).| } is set
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₁ where b₁ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T) : not the V11() real ext-real set <= |.(b₁ - the Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)).| } is set
c₂ is functional Element of bool the carrier of (TOP-REAL T)
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₁ where b₁ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T) : not X <= |.(b₁ - M).| } is 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
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₁ where b₁ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T) : not 1 <= |.(b₁ - (0. (TOP-REAL T))).| } is set
c₂ is functional open (T) Element of bool 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
c₂ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)
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₂,p) is non empty functional open Element of bool the carrier of (TOP-REAL T)
{ b₁ where b₁ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T) : not p <= |.(b₁ - c₂).| } is set
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₁ where b₁ 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 <= |.(b₁ - S1).| } is 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₂ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T)
M is V11() real ext-real set
Ball (c₂,M) is functional open Element of bool the carrier of (TOP-REAL T)
bool the carrier of (TOP-REAL T) is non empty set
{ b₁ where b₁ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T) : not M <= |.(b₁ - c₂).| } is set
(TOP-REAL T) | (Ball (c₂,M)) is 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
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₁ where b₁ is Relation-like NAT -defined Function-like V35() T -element V43() V44() V124() V125() V126() Element of the carrier of (TOP-REAL T) : not 1 <= |.(b₁ - (0. (TOP-REAL T))).| } is set
(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()