REAL is non empty non trivial V35() V183() V184() V185() V189() set
NAT is non empty non trivial ordinal V35() cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() Element of bool REAL
bool REAL is non empty non trivial V35() set
I[01] is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V231() pathwise_connected SubSpace of R^1
R^1 is non empty strict TopSpace-like V231() TopStruct
the carrier of I[01] is non empty V183() V184() V185() set
COMPLEX is non empty non trivial V35() V183() V189() set
omega is non empty non trivial ordinal V35() cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() set
bool omega is non empty non trivial V35() set
bool NAT is non empty non trivial V35() set
K194(NAT) is V53() set
1 is non empty ordinal natural V11() real ext-real positive non negative V35() cardinal V116() V117() V183() V184() V185() V186() V187() V188() Element of NAT
INT is non empty non trivial V35() V183() V184() V185() V186() V187() V189() set
[:1,1:] is non empty RAT -valued INT -valued V35() complex-yielding V174() V175() V176() set
RAT is non empty non trivial V35() V183() V184() V185() V186() V189() set
bool [:1,1:] is non empty V35() V39() set
[:[:1,1:],1:] is non empty RAT -valued INT -valued V35() complex-yielding V174() V175() V176() set
bool [:[:1,1:],1:] is non empty V35() V39() set
[:[:1,1:],REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [:[:1,1:],REAL:] is non empty non trivial V35() set
[:REAL,REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
[:[:REAL,REAL:],REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial V35() set
2 is non empty ordinal natural V11() real ext-real positive non negative V35() cardinal V116() V117() V183() V184() V185() V186() V187() V188() Element of NAT
[:2,2:] is non empty RAT -valued INT -valued V35() complex-yielding V174() V175() V176() set
[:[:2,2:],REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [:[:2,2:],REAL:] is non empty non trivial V35() set
bool [:REAL,REAL:] is non empty non trivial V35() set
K390() is non empty V132() L10()
the carrier of K390() is non empty set
K395() is non empty V132() V154() V155() V156() V158() V205() V206() V207() V208() V209() V210() L10()
K396() is non empty V132() V156() V158() V208() V209() V210() M15(K395())
K397() is non empty V132() V154() V156() V158() V208() V209() V210() V211() M18(K395(),K396())
K399() is non empty V132() V154() V156() V158() L10()
K400() is non empty V132() V154() V156() V158() V211() M15(K399())
K483() is non empty strict TopSpace-like T_0 T_1 T_2 connected compact V231() pathwise_connected TopStruct
the carrier of K483() is non empty V183() V184() V185() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V231() MetrStruct
real_dist is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
0 is empty trivial ordinal natural V11() real ext-real non positive non negative Function-like functional V35() V39() cardinal {} -element FinSequence-membered V116() V117() V183() V184() V185() V186() V187() V188() V189() Element of NAT
{} is empty trivial ordinal natural V11() real ext-real non positive non negative Function-like functional V35() V39() cardinal {} -element FinSequence-membered V183() V184() V185() V186() V187() V188() V189() set
the empty trivial ordinal natural V11() real ext-real non positive non negative Function-like functional V35() V39() cardinal {} -element FinSequence-membered V183() V184() V185() V186() V187() V188() V189() set is empty trivial ordinal natural V11() real ext-real non positive non negative Function-like functional V35() V39() cardinal {} -element FinSequence-membered V183() V184() V185() V186() V187() V188() V189() set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V231() SubSpace of R^1
the carrier of (Closed-Interval-TSpace (0,1)) is non empty V183() V184() V185() set
TOP-REAL 2 is non empty TopSpace-like V130() V195() V196() V233() V234() V235() V236() V237() V238() V239() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
the carrier of (TOP-REAL 2) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
[: the carrier of (TOP-REAL 2),REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [: the carrier of (TOP-REAL 2),REAL:] is non empty non trivial V35() set
bool the carrier of (TOP-REAL 2) is non empty set
the carrier of R^1 is non empty V183() V184() V185() set
{{},1} is non empty V35() V39() V183() V184() V185() V186() V187() V188() set
TOP-REAL 1 is non empty TopSpace-like V130() V195() V196() V233() V234() V235() V236() V237() V238() V239() strict RLTopStruct
the carrier of (TOP-REAL 1) is non empty set
[:COMPLEX,COMPLEX:] is non empty non trivial V35() complex-yielding set
bool [:COMPLEX,COMPLEX:] is non empty non trivial V35() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial V35() complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial V35() set
[:RAT,RAT:] is non empty non trivial RAT -valued V35() complex-yielding V174() V175() set
bool [:RAT,RAT:] is non empty non trivial V35() set
[:[:RAT,RAT:],RAT:] is non empty non trivial RAT -valued V35() complex-yielding V174() V175() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial V35() set
[:INT,INT:] is non empty non trivial RAT -valued INT -valued V35() complex-yielding V174() V175() set
bool [:INT,INT:] is non empty non trivial V35() set
[:[:INT,INT:],INT:] is non empty non trivial RAT -valued INT -valued V35() complex-yielding V174() V175() set
bool [:[:INT,INT:],INT:] is non empty non trivial V35() set
[:NAT,NAT:] is non empty non trivial RAT -valued INT -valued V35() complex-yielding V174() V175() V176() set
[:[:NAT,NAT:],NAT:] is non empty non trivial RAT -valued INT -valued V35() complex-yielding V174() V175() V176() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial V35() set
[:COMPLEX,REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [:COMPLEX,REAL:] is non empty non trivial V35() set
[:NAT,REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [:NAT,REAL:] is non empty non trivial V35() set
3 is non empty ordinal natural V11() real ext-real positive non negative V35() cardinal V116() V117() V183() V184() V185() V186() V187() V188() Element of NAT
0. (TOP-REAL 2) is Relation-like NAT -defined REAL -valued Function-like V35() 2 -element FinSequence-like FinSubsequence-like V62( TOP-REAL 2) complex-yielding V174() V175() Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is Relation-like NAT -defined REAL -valued Function-like V35() 2 -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL 2)
|[0,0]| is non empty Relation-like NAT -defined REAL -valued Function-like V35() 2 -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL 2)
REAL 0 is non empty functional FinSequence-membered FinSequenceSet of REAL
0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 0 } is set
TOP-REAL 0 is non empty TopSpace-like V130() V195() V196() V233() V234() V235() V236() V237() V238() V239() strict RLTopStruct
0. (TOP-REAL 0) is empty trivial ordinal natural V11() real ext-real non positive non negative Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional V35() V36() V39() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V62( TOP-REAL 0) complex-yielding V174() V175() V176() increasing V178() V179() V180() V183() V184() V185() V186() V187() V188() V189() Element of the carrier of (TOP-REAL 0)
the carrier of (TOP-REAL 0) is non empty set
the ZeroF of (TOP-REAL 0) is empty trivial ordinal natural V11() real ext-real non positive non negative Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional V35() V36() V39() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-yielding V174() V175() V176() increasing V178() V179() V180() V183() V184() V185() V186() V187() V188() V189() Element of the carrier of (TOP-REAL 0)
{(0. (TOP-REAL 0))} is non empty trivial functional V35() V39() 1 -element V183() V184() V185() V186() V187() V188() set
4 is non empty ordinal natural V11() real ext-real positive non negative V35() cardinal V116() V117() V183() V184() V185() V186() V187() V188() Element of NAT
[.0,1.] is V183() V184() V185() real-bounded Element of bool REAL
K484() is V11() real ext-real Element of the carrier of K483()
K485() is V11() real ext-real Element of the carrier of K483()
TopSpaceMetr RealSpace is TopStruct
sqrt 1 is V11() real ext-real Element of REAL
bool the carrier of R^1 is non empty set
(#) (0,1) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
(0,1) (#) is V11() real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))
Euclid 2 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL 2 is non empty functional FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 2 } is set
Pitag_dist 2 is non empty Relation-like [:(REAL 2),(REAL 2):] -defined REAL -valued Function-like total V30([:(REAL 2),(REAL 2):], REAL ) complex-yielding V174() V175() Element of bool [:[:(REAL 2),(REAL 2):],REAL:]
[:(REAL 2),(REAL 2):] is non empty set
[:[:(REAL 2),(REAL 2):],REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [:[:(REAL 2),(REAL 2):],REAL:] is non empty non trivial V35() set
MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct
the carrier of (Euclid 2) is non empty set
5 is non empty ordinal natural V11() real ext-real positive non negative V35() cardinal V116() V117() V183() V184() V185() V186() V187() V188() Element of NAT
multreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
C is ordinal natural V11() real ext-real non negative V35() cardinal set
TOP-REAL C is non empty TopSpace-like V130() V195() V196() V233() V234() V235() V236() V237() V238() V239() strict RLTopStruct
Euclid C is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL C is non empty functional FinSequence-membered FinSequenceSet of REAL
C -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = C } is set
Pitag_dist C is non empty Relation-like [:(REAL C),(REAL C):] -defined REAL -valued Function-like total V30([:(REAL C),(REAL C):], REAL ) complex-yielding V174() V175() Element of bool [:[:(REAL C),(REAL C):],REAL:]
[:(REAL C),(REAL C):] is non empty set
[:[:(REAL C),(REAL C):],REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [:[:(REAL C),(REAL C):],REAL:] is non empty non trivial V35() set
MetrStruct(# (REAL C),(Pitag_dist C) #) is strict MetrStruct
TopSpaceMetr (Euclid C) is TopStruct
the carrier of (TOP-REAL C) is non empty set
the topology of (TOP-REAL C) is non empty Element of bool (bool the carrier of (TOP-REAL C))
bool the carrier of (TOP-REAL C) is non empty set
bool (bool the carrier of (TOP-REAL C)) is non empty set
TopStruct(# the carrier of (TOP-REAL C), the topology of (TOP-REAL C) #) is non empty strict TopSpace-like TopStruct
C is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
r is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
K258((TOP-REAL C),C,r) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
the U7 of (TOP-REAL C) is non empty Relation-like [: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):] -defined the carrier of (TOP-REAL C) -valued Function-like total V30([: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):], the carrier of (TOP-REAL C)) Element of bool [:[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):], the carrier of (TOP-REAL C):]
[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):] is non empty set
[:[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):], the carrier of (TOP-REAL C):] is non empty set
bool [:[: the carrier of (TOP-REAL C), the carrier of (TOP-REAL C):], the carrier of (TOP-REAL C):] is non empty set
the U7 of (TOP-REAL C) . (C,r) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
[C,r] is non empty set
{C,r} is non empty functional V35() V39() set
{C} is non empty trivial functional V35() V39() 1 -element set
{{C,r},{C}} is non empty V35() V39() set
the U7 of (TOP-REAL C) . [C,r] is set
C + r is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
addreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
addreal .: (C,r) is set
EX2 is Element of bool the carrier of (TOP-REAL C)
C + r is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
the carrier of (Euclid C) is non empty set
the carrier of (TopSpaceMetr (Euclid C)) is set
bool the carrier of (TopSpaceMetr (Euclid C)) is non empty set
t2 is Element of bool the carrier of (TopSpaceMetr (Euclid C))
EX is Element of the carrier of (Euclid C)
qt2 is V11() real ext-real set
Ball (EX,qt2) is bounded Element of bool the carrier of (Euclid C)
bool the carrier of (Euclid C) is non empty set
qt2 / 2 is V11() real ext-real Element of REAL
EX1 is Element of the carrier of (Euclid C)
Ball (EX1,(qt2 / 2)) is bounded Element of bool the carrier of (Euclid C)
p1 is Element of the carrier of (Euclid C)
Ball (p1,(qt2 / 2)) is bounded Element of bool the carrier of (Euclid C)
q4 is Element of bool the carrier of (TOP-REAL C)
r5 is Element of bool the carrier of (TOP-REAL C)
q4 + r5 is Element of bool the carrier of (TOP-REAL C)
r0 is set
q4 + r5 is Element of bool the carrier of (TOP-REAL C)
{ (b1 + b2) where b1, b2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C) : ( b1 in q4 & b2 in r5 ) } is set
Q is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
P3 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
Q + P3 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
the U7 of (TOP-REAL C) . (Q,P3) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
[Q,P3] is non empty set
{Q,P3} is non empty functional V35() V39() set
{Q} is non empty trivial functional V35() V39() 1 -element set
{{Q,P3},{Q}} is non empty V35() V39() set
the U7 of (TOP-REAL C) . [Q,P3] is set
Q + P3 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
addreal .: (Q,P3) is set
Q is Element of the carrier of (Euclid C)
dist (p1,Q) is V11() real ext-real Element of REAL
the distance of (Euclid C) is non empty Relation-like [: the carrier of (Euclid C), the carrier of (Euclid C):] -defined REAL -valued Function-like total V30([: the carrier of (Euclid C), the carrier of (Euclid C):], REAL ) complex-yielding V174() V175() Element of bool [:[: the carrier of (Euclid C), the carrier of (Euclid C):],REAL:]
[: the carrier of (Euclid C), the carrier of (Euclid C):] is non empty set
[:[: the carrier of (Euclid C), the carrier of (Euclid C):],REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [:[: the carrier of (Euclid C), the carrier of (Euclid C):],REAL:] is non empty non trivial V35() set
the distance of (Euclid C) . (p1,Q) is V11() real ext-real Element of REAL
[p1,Q] is non empty set
{p1,Q} is non empty V35() set
{p1} is non empty trivial V35() 1 -element set
{{p1,Q},{p1}} is non empty V35() V39() set
the distance of (Euclid C) . [p1,Q] is V11() real ext-real set
z is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
r is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
z - r is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
diffreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total V30( REAL , REAL ) complex-yielding V174() V175() increasing V179() Element of bool [:REAL,REAL:]
compreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
K174(REAL,addreal,(id REAL),compreal) is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
diffreal .: (z,r) is set
K324(r) is Relation-like Function-like complex-yielding set
r (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) is V11() real ext-real non positive set
K38(1) * r is Relation-like Function-like set
K38(1) multreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
multreal [;] (K38(1),(id REAL)) is set
r (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295(z,K324(r)) is Relation-like Function-like set
|.(z - r).| is V11() real ext-real non negative Element of REAL
sqr (z - r) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
(z - r) (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt ((z - r),(z - r)) is Relation-like Function-like set
multreal .: ((z - r),(z - r)) is set
K383((sqr (z - r))) is V11() real ext-real Element of REAL
K195(REAL,(sqr (z - r)),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr (z - r))) is V11() real ext-real Element of REAL
W3 is Element of the carrier of (Euclid C)
dist (EX1,W3) is V11() real ext-real Element of REAL
the distance of (Euclid C) . (EX1,W3) is V11() real ext-real Element of REAL
[EX1,W3] is non empty set
{EX1,W3} is non empty V35() set
{EX1} is non empty trivial V35() 1 -element set
{{EX1,W3},{EX1}} is non empty V35() V39() set
the distance of (Euclid C) . [EX1,W3] is V11() real ext-real set
W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
q is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
W2 - q is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
diffreal .: (W2,q) is set
K324(q) is Relation-like Function-like complex-yielding set
q (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * q is Relation-like Function-like set
q (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295(W2,K324(q)) is Relation-like Function-like set
|.(W2 - q).| is V11() real ext-real non negative Element of REAL
sqr (W2 - q) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
(W2 - q) (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt ((W2 - q),(W2 - q)) is Relation-like Function-like set
multreal .: ((W2 - q),(W2 - q)) is set
K383((sqr (W2 - q))) is V11() real ext-real Element of REAL
K195(REAL,(sqr (W2 - q)),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr (W2 - q))) is V11() real ext-real Element of REAL
(qt2 / 2) + (qt2 / 2) is V11() real ext-real Element of REAL
|.(W2 - q).| + |.(z - r).| is V11() real ext-real non negative Element of REAL
W2 + z is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (W2,z) is set
q + r is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (q,r) is set
(W2 + z) - (q + r) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
diffreal .: ((W2 + z),(q + r)) is set
K324((q + r)) is Relation-like Function-like complex-yielding set
(q + r) (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * (q + r) is Relation-like Function-like set
(q + r) (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295((W2 + z),K324((q + r))) is Relation-like Function-like set
r + q is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (r,q) is set
- (r + q) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(r + q) (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * (r + q) is Relation-like Function-like set
(r + q) (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(W2 + z) + (- (r + q)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((W2 + z),(- (r + q))) is set
- r is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
- q is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(- r) + (- q) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((- r),(- q)) is set
(W2 + z) + ((- r) + (- q)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((W2 + z),((- r) + (- q))) is set
(W2 + z) + (- r) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((W2 + z),(- r)) is set
((W2 + z) + (- r)) + (- q) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (((W2 + z) + (- r)),(- q)) is set
z + (- r) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (z,(- r)) is set
(z + (- r)) + W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((z + (- r)),W2) is set
((z + (- r)) + W2) + (- q) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (((z + (- r)) + W2),(- q)) is set
W2 + (- q) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (W2,(- q)) is set
(z + (- r)) + (W2 + (- q)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((z + (- r)),(W2 + (- q))) is set
(z - r) + (W2 + (- q)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((z - r),(W2 + (- q))) is set
(z - r) + (W2 - q) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((z - r),(W2 - q)) is set
P2 is Element of the carrier of (Euclid C)
dist (EX,P2) is V11() real ext-real Element of REAL
the distance of (Euclid C) . (EX,P2) is V11() real ext-real Element of REAL
[EX,P2] is non empty set
{EX,P2} is non empty V35() set
{EX} is non empty trivial V35() 1 -element set
{{EX,P2},{EX}} is non empty V35() V39() set
the distance of (Euclid C) . [EX,P2] is V11() real ext-real set
(W2 - q) + (z - r) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((W2 - q),(z - r)) is set
|.((W2 - q) + (z - r)).| is V11() real ext-real non negative Element of REAL
sqr ((W2 - q) + (z - r)) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
((W2 - q) + (z - r)) (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt (((W2 - q) + (z - r)),((W2 - q) + (z - r))) is Relation-like Function-like set
multreal .: (((W2 - q) + (z - r)),((W2 - q) + (z - r))) is set
K383((sqr ((W2 - q) + (z - r)))) is V11() real ext-real Element of REAL
K195(REAL,(sqr ((W2 - q) + (z - r))),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr ((W2 - q) + (z - r)))) is V11() real ext-real Element of REAL
C is V11() real ext-real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
C * r is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
C * r is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
C multreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total V30( REAL , REAL ) complex-yielding V174() V175() increasing V179() Element of bool [:REAL,REAL:]
multreal [;] (C,(id REAL)) is set
r (#) (C multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
EX2 is Element of bool the carrier of (TOP-REAL C)
the carrier of (Euclid C) is non empty set
the carrier of (TopSpaceMetr (Euclid C)) is set
bool the carrier of (TopSpaceMetr (Euclid C)) is non empty set
EX is Element of bool the carrier of (TopSpaceMetr (Euclid C))
p1 is Element of the carrier of (Euclid C)
t2 is V11() real ext-real set
Ball (p1,t2) is bounded Element of bool the carrier of (Euclid C)
bool the carrier of (Euclid C) is non empty set
t2 / 2 is V11() real ext-real Element of REAL
(t2 / 2) / 2 is V11() real ext-real Element of REAL
abs C is V11() real ext-real Element of REAL
(abs C) * 1 is V11() real ext-real Element of REAL
((t2 / 2) / 2) / (abs C) is V11() real ext-real Element of REAL
r2 is non empty V11() real ext-real positive non negative Element of REAL
(abs C) * r2 is V11() real ext-real Element of REAL
r2 is non empty V11() real ext-real positive non negative Element of REAL
(abs C) * r2 is V11() real ext-real Element of REAL
r2 is non empty V11() real ext-real positive non negative Element of REAL
(abs C) * r2 is V11() real ext-real Element of REAL
EX1 is Element of the carrier of (Euclid C)
Ball (EX1,r2) is bounded Element of bool the carrier of (Euclid C)
|.r.| is V11() real ext-real non negative Element of REAL
sqr r is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
r (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt (r,r) is Relation-like Function-like set
multreal .: (r,r) is set
K383((sqr r)) is V11() real ext-real Element of REAL
addreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
K195(REAL,(sqr r),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr r)) is V11() real ext-real Element of REAL
|.r.| + r2 is non empty V11() real ext-real positive non negative Element of REAL
(t2 / 2) / (|.r.| + r2) is V11() real ext-real Element of REAL
r5 is non empty V11() real ext-real positive non negative Element of REAL
q4 is Element of bool the carrier of (TOP-REAL C)
r0 is V11() real ext-real Element of REAL
r0 - C is V11() real ext-real Element of REAL
abs (r0 - C) is V11() real ext-real Element of REAL
r0 * q4 is Element of bool the carrier of (TOP-REAL C)
{ (r0 * b1) where b1 is Element of the carrier of (TOP-REAL C) : b1 in q4 } is set
Q is set
P3 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
r0 * P3 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
r0 * P3 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
r0 multreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
multreal [;] (r0,(id REAL)) is set
P3 (#) (r0 multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
P2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
q is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
C |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() V176() Element of C -tuples_on NAT
C -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like V35() FinSequence-like FinSubsequence-like Element of NAT * : len b1 = C } is set
Seg C is V35() C -element V183() V184() V185() V186() V187() V188() Element of bool NAT
(Seg C) --> 0 is Relation-like Seg C -defined INT -valued RAT -valued {0} -valued Function-like total V30( Seg C,{0}) V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() V176() Element of bool [:(Seg C),{0}:]
{0} is non empty trivial V35() V39() 1 -element V183() V184() V185() V186() V187() V188() set
[:(Seg C),{0}:] is INT -valued RAT -valued V35() complex-yielding V174() V175() V176() set
bool [:(Seg C),{0}:] is non empty V35() V39() set
q - (C |-> 0) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
diffreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
compreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
K174(REAL,addreal,(id REAL),compreal) is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
diffreal .: (q,(C |-> 0)) is set
K324((C |-> 0)) is Relation-like Function-like complex-yielding set
(C |-> 0) (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) is V11() real ext-real non positive set
K38(1) * (C |-> 0) is Relation-like Function-like set
K38(1) multreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
multreal [;] (K38(1),(id REAL)) is set
(C |-> 0) (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295(q,K324((C |-> 0))) is Relation-like Function-like set
z is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
z - z is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
diffreal .: (z,z) is set
K324(z) is Relation-like Function-like complex-yielding set
z (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * z is Relation-like Function-like set
z (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295(z,K324(z)) is Relation-like Function-like set
q - (z - z) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
diffreal .: (q,(z - z)) is set
K324((z - z)) is Relation-like Function-like complex-yielding set
(z - z) (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * (z - z) is Relation-like Function-like set
(z - z) (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295(q,K324((z - z))) is Relation-like Function-like set
q - z is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
diffreal .: (q,z) is set
K295(q,K324(z)) is Relation-like Function-like set
(q - z) + z is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
addreal .: ((q - z),z) is set
|.W2.| is V11() real ext-real non negative Element of REAL
sqr W2 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
W2 (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt (W2,W2) is Relation-like Function-like set
multreal .: (W2,W2) is set
K383((sqr W2)) is V11() real ext-real Element of REAL
K195(REAL,(sqr W2),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr W2)) is V11() real ext-real Element of REAL
W2 - P2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
diffreal .: (W2,P2) is set
K324(P2) is Relation-like Function-like complex-yielding set
P2 (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * P2 is Relation-like Function-like set
P2 (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295(W2,K324(P2)) is Relation-like Function-like set
|.(W2 - P2).| is V11() real ext-real non negative Element of REAL
sqr (W2 - P2) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
(W2 - P2) (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt ((W2 - P2),(W2 - P2)) is Relation-like Function-like set
multreal .: ((W2 - P2),(W2 - P2)) is set
K383((sqr (W2 - P2))) is V11() real ext-real Element of REAL
K195(REAL,(sqr (W2 - P2)),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr (W2 - P2))) is V11() real ext-real Element of REAL
|.P2.| is V11() real ext-real non negative Element of REAL
sqr P2 is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
P2 (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt (P2,P2) is Relation-like Function-like set
multreal .: (P2,P2) is set
K383((sqr P2)) is V11() real ext-real Element of REAL
K195(REAL,(sqr P2),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr P2)) is V11() real ext-real Element of REAL
|.(W2 - P2).| + |.P2.| is V11() real ext-real non negative Element of REAL
W3 is Element of the carrier of (Euclid C)
dist (EX1,W3) is V11() real ext-real Element of REAL
the distance of (Euclid C) is non empty Relation-like [: the carrier of (Euclid C), the carrier of (Euclid C):] -defined REAL -valued Function-like total V30([: the carrier of (Euclid C), the carrier of (Euclid C):], REAL ) complex-yielding V174() V175() Element of bool [:[: the carrier of (Euclid C), the carrier of (Euclid C):],REAL:]
[: the carrier of (Euclid C), the carrier of (Euclid C):] is non empty set
[:[: the carrier of (Euclid C), the carrier of (Euclid C):],REAL:] is non empty non trivial V35() complex-yielding V174() V175() set
bool [:[: the carrier of (Euclid C), the carrier of (Euclid C):],REAL:] is non empty non trivial V35() set
the distance of (Euclid C) . (EX1,W3) is V11() real ext-real Element of REAL
[EX1,W3] is non empty set
{EX1,W3} is non empty V35() set
{EX1} is non empty trivial V35() 1 -element set
{{EX1,W3},{EX1}} is non empty V35() V39() set
the distance of (Euclid C) . [EX1,W3] is V11() real ext-real set
r2 + |.r.| is non empty V11() real ext-real positive non negative Element of REAL
r5 * |.W2.| is V11() real ext-real non negative Element of REAL
r5 * (r2 + |.r.|) is V11() real ext-real non negative Element of REAL
C * P2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
P2 (#) (C multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
C * W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
W2 (#) (C multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
- (C * W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(C * W2) (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * (C * W2) is Relation-like Function-like set
(C * W2) (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(C * P2) + (- (C * W2)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((C * P2),(- (C * W2))) is set
- 1 is V11() real ext-real non positive Element of REAL
(- 1) * (C * W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(- 1) multreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
multreal [;] ((- 1),(id REAL)) is set
(C * W2) (#) ((- 1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(C * P2) + ((- 1) * (C * W2)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((C * P2),((- 1) * (C * W2))) is set
(- 1) * C is V11() real ext-real Element of REAL
((- 1) * C) * W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
((- 1) * C) multreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
multreal [;] (((- 1) * C),(id REAL)) is set
W2 (#) (((- 1) * C) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(C * P2) + (((- 1) * C) * W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((C * P2),(((- 1) * C) * W2)) is set
(- 1) * W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
W2 (#) ((- 1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
C * ((- 1) * W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
((- 1) * W2) (#) (C multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(C * P2) + (C * ((- 1) * W2)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((C * P2),(C * ((- 1) * W2))) is set
P2 + ((- 1) * W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (P2,((- 1) * W2)) is set
C * (P2 + ((- 1) * W2)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(P2 + ((- 1) * W2)) (#) (C multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
- W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
W2 (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * W2 is Relation-like Function-like set
W2 (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
P2 + (- W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (P2,(- W2)) is set
C * (P2 + (- W2)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(P2 + (- W2)) (#) (C multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
P2 - W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
diffreal .: (P2,W2) is set
K324(W2) is Relation-like Function-like complex-yielding set
K295(P2,K324(W2)) is Relation-like Function-like set
C * (P2 - W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(P2 - W2) (#) (C multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
|.((C * P2) + (- (C * W2))).| is V11() real ext-real non negative Element of REAL
sqr ((C * P2) + (- (C * W2))) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
((C * P2) + (- (C * W2))) (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt (((C * P2) + (- (C * W2))),((C * P2) + (- (C * W2)))) is Relation-like Function-like set
multreal .: (((C * P2) + (- (C * W2))),((C * P2) + (- (C * W2)))) is set
K383((sqr ((C * P2) + (- (C * W2))))) is V11() real ext-real Element of REAL
K195(REAL,(sqr ((C * P2) + (- (C * W2)))),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr ((C * P2) + (- (C * W2))))) is V11() real ext-real Element of REAL
|.(P2 - W2).| is V11() real ext-real non negative Element of REAL
sqr (P2 - W2) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
(P2 - W2) (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt ((P2 - W2),(P2 - W2)) is Relation-like Function-like set
multreal .: ((P2 - W2),(P2 - W2)) is set
K383((sqr (P2 - W2))) is V11() real ext-real Element of REAL
K195(REAL,(sqr (P2 - W2)),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr (P2 - W2))) is V11() real ext-real Element of REAL
(abs C) * |.(P2 - W2).| is V11() real ext-real Element of REAL
r0 * W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
W2 (#) (r0 multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
- (r0 * W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(r0 * W2) (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * (r0 * W2) is Relation-like Function-like set
(r0 * W2) (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(C * W2) + (- (r0 * W2)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((C * W2),(- (r0 * W2))) is set
(- 1) * (r0 * W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(r0 * W2) (#) ((- 1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(C * W2) + ((- 1) * (r0 * W2)) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((C * W2),((- 1) * (r0 * W2))) is set
(- 1) * r0 is V11() real ext-real Element of REAL
((- 1) * r0) * W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
((- 1) * r0) multreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
multreal [;] (((- 1) * r0),(id REAL)) is set
W2 (#) (((- 1) * r0) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(C * W2) + (((- 1) * r0) * W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: ((C * W2),(((- 1) * r0) * W2)) is set
C + ((- 1) * r0) is V11() real ext-real Element of REAL
(C + ((- 1) * r0)) * W2 is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
(C + ((- 1) * r0)) multreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
multreal [;] ((C + ((- 1) * r0)),(id REAL)) is set
W2 (#) ((C + ((- 1) * r0)) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
|.((C * W2) + (- (r0 * W2))).| is V11() real ext-real non negative Element of REAL
sqr ((C * W2) + (- (r0 * W2))) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
((C * W2) + (- (r0 * W2))) (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt (((C * W2) + (- (r0 * W2))),((C * W2) + (- (r0 * W2)))) is Relation-like Function-like set
multreal .: (((C * W2) + (- (r0 * W2))),((C * W2) + (- (r0 * W2)))) is set
K383((sqr ((C * W2) + (- (r0 * W2))))) is V11() real ext-real Element of REAL
K195(REAL,(sqr ((C * W2) + (- (r0 * W2)))),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr ((C * W2) + (- (r0 * W2))))) is V11() real ext-real Element of REAL
C - r0 is V11() real ext-real Element of REAL
abs (C - r0) is V11() real ext-real Element of REAL
(abs (C - r0)) * |.W2.| is V11() real ext-real Element of REAL
- (C - r0) is V11() real ext-real Element of REAL
abs (- (C - r0)) is V11() real ext-real Element of REAL
(abs (- (C - r0))) * |.W2.| is V11() real ext-real Element of REAL
r5 * (|.r.| + r2) is V11() real ext-real non negative Element of REAL
((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2))) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
addreal .: (((C * P2) + (- (C * W2))),((C * W2) + (- (r0 * W2)))) is set
|.(((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2)))).| is V11() real ext-real non negative Element of REAL
sqr (((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2)))) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
(((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2)))) (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt ((((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2)))),(((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2))))) is Relation-like Function-like set
multreal .: ((((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2)))),(((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2))))) is set
K383((sqr (((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2)))))) is V11() real ext-real Element of REAL
K195(REAL,(sqr (((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2))))),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr (((C * P2) + (- (C * W2))) + ((C * W2) + (- (r0 * W2)))))) is V11() real ext-real Element of REAL
|.((C * P2) + (- (C * W2))).| + |.((C * W2) + (- (r0 * W2))).| is V11() real ext-real non negative Element of REAL
(t2 / 2) + (t2 / 2) is V11() real ext-real Element of REAL
(C * P2) - (r0 * W2) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of REAL C
diffreal .: ((C * P2),(r0 * W2)) is set
K324((r0 * W2)) is Relation-like Function-like complex-yielding set
K295((C * P2),K324((r0 * W2))) is Relation-like Function-like set
C * z is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
z (#) (C multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(C * z) - (C |-> 0) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
diffreal .: ((C * z),(C |-> 0)) is set
K295((C * z),K324((C |-> 0))) is Relation-like Function-like set
r0 * q is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
q (#) (r0 multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
((C * z) - (C |-> 0)) - (r0 * q) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
diffreal .: (((C * z) - (C |-> 0)),(r0 * q)) is set
K324((r0 * q)) is Relation-like Function-like complex-yielding set
(r0 * q) (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * (r0 * q) is Relation-like Function-like set
(r0 * q) (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295(((C * z) - (C |-> 0)),K324((r0 * q))) is Relation-like Function-like set
C * q is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
q (#) (C multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
(C * q) - (C * q) is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of C -tuples_on REAL
diffreal .: ((C * q),(C * q)) is set
K324((C * q)) is Relation-like Function-like complex-yielding set
(C * q) (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * (C * q) is Relation-like Function-like set
(C * q) (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295((C * q),K324((C * q))) is Relation-like Function-like set
(C * P2) - ((C * q) - (C * q)) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
diffreal .: ((C * P2),((C * q) - (C * q))) is set
K324(((C * q) - (C * q))) is Relation-like Function-like complex-yielding set
((C * q) - (C * q)) (#) compreal is Relation-like Function-like V35() complex-yielding V174() V175() set
K38(1) * ((C * q) - (C * q)) is Relation-like Function-like set
((C * q) - (C * q)) (#) (K38(1) multreal) is Relation-like Function-like V35() complex-yielding V174() V175() set
K295((C * P2),K324(((C * q) - (C * q)))) is Relation-like Function-like set
((C * P2) - ((C * q) - (C * q))) - (r0 * W2) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
diffreal .: (((C * P2) - ((C * q) - (C * q))),(r0 * W2)) is set
K295(((C * P2) - ((C * q) - (C * q))),K324((r0 * W2))) is Relation-like Function-like set
(C * P2) - (C * q) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
diffreal .: ((C * P2),(C * q)) is set
K295((C * P2),K324((C * q))) is Relation-like Function-like set
((C * P2) - (C * q)) + (C * q) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
addreal .: (((C * P2) - (C * q)),(C * q)) is set
(((C * P2) - (C * q)) + (C * q)) - (r0 * W2) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
diffreal .: ((((C * P2) - (C * q)) + (C * q)),(r0 * W2)) is set
K295((((C * P2) - (C * q)) + (C * q)),K324((r0 * W2))) is Relation-like Function-like set
(((C * P2) - (C * q)) + (C * q)) + (- (r0 * W2)) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
addreal .: ((((C * P2) - (C * q)) + (C * q)),(- (r0 * W2))) is set
((C * P2) - (C * q)) + ((C * W2) + (- (r0 * W2))) is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
addreal .: (((C * P2) - (C * q)),((C * W2) + (- (r0 * W2)))) is set
Q is Element of the carrier of (Euclid C)
dist (p1,Q) is V11() real ext-real Element of REAL
the distance of (Euclid C) . (p1,Q) is V11() real ext-real Element of REAL
[p1,Q] is non empty set
{p1,Q} is non empty V35() set
{p1} is non empty trivial V35() 1 -element set
{{p1,Q},{p1}} is non empty V35() V39() set
the distance of (Euclid C) . [p1,Q] is V11() real ext-real set
C is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
{C,p} is non empty V35() V183() V184() V185() Element of bool REAL
WH is Relation-like NAT -defined REAL -valued Function-like one-to-one V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() increasing V179() FinSequence of REAL
rng WH is V35() V183() V184() V185() Element of bool REAL
len WH is ordinal natural V11() real ext-real non negative V35() cardinal V116() V117() V183() V184() V185() V186() V187() V188() Element of NAT
WH . 1 is V11() real ext-real Element of REAL
WH . 2 is V11() real ext-real Element of REAL
dom WH is V35() V183() V184() V185() V186() V187() V188() Element of bool NAT
C is ordinal natural V11() real ext-real non negative V35() cardinal V116() V117() V183() V184() V185() V186() V187() V188() Element of NAT
TOP-REAL C is non empty TopSpace-like V130() V195() V196() V233() V234() V235() V236() V237() V238() V239() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty set
p is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
|.p.| is V11() real ext-real non negative Element of REAL
sqr p is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
p (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt (p,p) is Relation-like Function-like set
multreal .: (p,p) is set
K383((sqr p)) is V11() real ext-real Element of REAL
addreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
K195(REAL,(sqr p),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr p)) is V11() real ext-real Element of REAL
abs |.p.| is V11() real ext-real Element of REAL
C is ordinal natural V11() real ext-real non negative V35() cardinal V116() V117() V183() V184() V185() V186() V187() V188() Element of NAT
TOP-REAL C is non empty TopSpace-like V130() V195() V196() V233() V234() V235() V236() V237() V238() V239() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL C) is non empty set
p is Relation-like NAT -defined REAL -valued Function-like V35() C -element FinSequence-like FinSubsequence-like complex-yielding V174() V175() Element of the carrier of (TOP-REAL C)
|.p.| is V11() real ext-real non negative Element of REAL
sqr p is Relation-like NAT -defined REAL -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V174() V175() FinSequence of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V174() V175() Element of bool [:REAL,REAL:]
p (#) sqrreal is Relation-like Function-like V35() complex-yielding V174() V175() set
mlt (p,p) is Relation-like Function-like set
multreal .: (p,p) is set
K383((sqr p)) is V11() real ext-real Element of REAL
addreal is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V30([:REAL,REAL:], REAL ) complex-yielding V174() V175() Element of bool [:[:REAL,REAL:],REAL:]
K195(REAL,(sqr p),addreal) is V11() real ext-real Element of REAL
sqrt K383((sqr<