REAL is V46() V47() V48() V52() set
NAT is non empty V27() V28() V29() V46() V47() V48() V49() V50() V51() V52() Element of bool REAL
bool REAL is non empty set
COMPLEX is V46() V52() set
NAT is non empty V27() V28() V29() V46() V47() V48() V49() V50() V51() V52() set
bool NAT is non empty set
bool NAT is non empty set
1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is non empty set
{} is set
the empty functional V27() V28() V29() V31() V32() V33() ext-real non positive non negative V46() V47() V48() V49() V50() V51() V52() finite V59() FinSequence-membered set is empty functional V27() V28() V29() V31() V32() V33() ext-real non positive non negative V46() V47() V48() V49() V50() V51() V52() finite V59() FinSequence-membered set
3 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
0 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
PT is Relation-like set
metr is set
PT |_2 metr is Relation-like set
[:metr,metr:] is set
PT /\ [:metr,metr:] is set
field (PT |_2 metr) is set
FX is set
[FX,FX] is set
{FX,FX} is finite set
{FX} is finite set
{{FX,FX},{FX}} is finite V59() set
FX is set
R is set
[FX,R] is set
{FX,R} is finite set
{FX} is finite set
{{FX,R},{FX}} is finite V59() set
[R,FX] is set
{R,FX} is finite set
{R} is finite set
{{R,FX},{R}} is finite V59() set
FX is set
R is set
[FX,R] is set
{FX,R} is finite set
{FX} is finite set
{{FX,R},{FX}} is finite V59() set
[R,FX] is set
{R,FX} is finite set
{R} is finite set
{{R,FX},{R}} is finite V59() set
FX is set
R is set
PT -Seg R is set
Coim (PT,R) is set
{R} is finite set
(Coim (PT,R)) \ {R} is Element of bool (Coim (PT,R))
bool (Coim (PT,R)) is non empty set
(PT |_2 metr) -Seg R is set
Coim ((PT |_2 metr),R) is set
(Coim ((PT |_2 metr),R)) \ {R} is Element of bool (Coim ((PT |_2 metr),R))
bool (Coim ((PT |_2 metr),R)) is non empty set
FX is set
[FX,FX] is set
{FX,FX} is finite set
{FX} is finite set
{{FX,FX},{FX}} is finite V59() set
FX is set
R is set
Mn is set
[FX,R] is set
{FX,R} is finite set
{FX} is finite set
{{FX,R},{FX}} is finite V59() set
[R,Mn] is set
{R,Mn} is finite set
{R} is finite set
{{R,Mn},{R}} is finite V59() set
[FX,Mn] is set
{FX,Mn} is finite set
{{FX,Mn},{FX}} is finite V59() set
F2() is Relation-like set
F1() is set
PT is set
metr is set
metr is set
metr is set
metr is set
metr is set
FX is set
[metr,FX] is set
{metr,FX} is finite set
{metr} is finite set
{{metr,FX},{metr}} is finite V59() set
PT is set
metr is Relation-like set
FX is Element of PT
metr -Seg FX is set
Coim (metr,FX) is set
{FX} is finite set
(Coim (metr,FX)) \ {FX} is Element of bool (Coim (metr,FX))
bool (Coim (metr,FX)) is non empty set
union (metr -Seg FX) is set
PT is set
metr is Relation-like set
union PT is set
bool (union PT) is non empty Element of bool (bool (union PT))
bool (union PT) is non empty set
bool (bool (union PT)) is non empty set
FX is set
R is set
Mn is set
PM is Element of PT
(PT,metr,PM) is set
metr -Seg PM is set
Coim (metr,PM) is set
{PM} is finite set
(Coim (metr,PM)) \ {PM} is Element of bool (Coim (metr,PM))
bool (Coim (metr,PM)) is non empty set
union (metr -Seg PM) is set
PM \ (PT,metr,PM) is Element of bool PM
bool PM is non empty set
PM is Element of PT
(PT,metr,PM) is set
metr -Seg PM is set
Coim (metr,PM) is set
{PM} is finite set
(Coim (metr,PM)) \ {PM} is Element of bool (Coim (metr,PM))
bool (Coim (metr,PM)) is non empty set
union (metr -Seg PM) is set
PM \ (PT,metr,PM) is Element of bool PM
bool PM is non empty set
PT is set
bool PT is non empty Element of bool (bool PT)
bool PT is non empty set
bool (bool PT) is non empty set
[:NAT,(bool PT):] is non empty set
bool [:NAT,(bool PT):] is non empty set
FX is Relation-like NAT -defined bool PT -valued Function-like V43( NAT , bool PT) Element of bool [:NAT,(bool PT):]
metr is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
Seg metr is V46() V47() V48() V49() V50() V51() finite V62(metr) Element of bool NAT
{metr} is V46() V47() V48() V49() V50() V51() finite set
(Seg metr) \ {metr} is V46() V47() V48() V49() V50() V51() finite Element of bool NAT
FX .: ((Seg metr) \ {metr}) is finite set
union (FX .: ((Seg metr) \ {metr})) is set
PT is non empty TopSpace-like TopStruct
the carrier of PT is non empty set
bool the carrier of PT is non empty set
bool (bool the carrier of PT) is non empty set
metr is Element of bool (bool the carrier of PT)
FX is Element of bool (bool the carrier of PT)
R is Element of bool the carrier of PT
Mn is Element of bool the carrier of PT
PM is Element of bool the carrier of PT
Cl Mn is closed Element of bool the carrier of PT
union FX is Element of bool the carrier of PT
R is set
Mn is Element of the carrier of PT
PM is Element of bool the carrier of PT
PM is Element of bool the carrier of PT
PM ` is Element of bool the carrier of PT
(PM `) ` is Element of bool the carrier of PT
UB is Element of bool the carrier of PT
UB is Element of bool the carrier of PT
UB ` is Element of bool the carrier of PT
Cl UB is closed Element of bool the carrier of PT
PM is Element of bool the carrier of PT
PM ` is Element of bool the carrier of PT
[#] PT is non empty non proper open closed Element of bool the carrier of PT
UB is Element of bool the carrier of PT
{} PT is empty proper functional V27() V28() V29() V31() V32() V33() ext-real non positive non negative V46() V47() V48() V49() V50() V51() V52() finite V59() FinSequence-membered open closed Element of bool the carrier of PT
({} PT) ` is open closed Element of bool the carrier of PT
Cl UB is closed Element of bool the carrier of PT
PM is Element of bool the carrier of PT
PM ` is Element of bool the carrier of PT
R is Element of bool the carrier of PT
Cl R is closed Element of bool the carrier of PT
Mn is Element of bool the carrier of PT
PM is Element of bool the carrier of PT
Cl Mn is closed Element of bool the carrier of PT
PT is non empty TopSpace-like TopStruct
the carrier of PT is non empty set
bool the carrier of PT is non empty set
bool (bool the carrier of PT) is non empty set
metr is Element of bool (bool the carrier of PT)
FX is Element of bool (bool the carrier of PT)
R is Element of bool (bool the carrier of PT)
Mn is Element of bool the carrier of PT
Cl Mn is closed Element of bool the carrier of PT
PM is set
PM is Element of bool the carrier of PT
Cl PM is closed Element of bool the carrier of PT
UB is Element of bool the carrier of PT
clf R is Element of bool (bool the carrier of PT)
Mn is set
PM is Element of bool the carrier of PT
PM is Element of bool the carrier of PT
Cl PM is closed Element of bool the carrier of PT
UB is Element of bool the carrier of PT
PT is non empty TopSpace-like TopStruct
the carrier of PT is non empty set
[: the carrier of PT, the carrier of PT:] is non empty set
[:[: the carrier of PT, the carrier of PT:],REAL:] is set
bool [:[: the carrier of PT, the carrier of PT:],REAL:] is non empty set
metr is Reflexive discerning symmetric triangle MetrStruct
the carrier of metr is set
FX is Relation-like [: the carrier of PT, the carrier of PT:] -defined REAL -valued Function-like V43([: the carrier of PT, the carrier of PT:], REAL ) Element of bool [:[: the carrier of PT, the carrier of PT:],REAL:]
SpaceMetr ( the carrier of PT,FX) is strict Reflexive discerning symmetric triangle MetrStruct
MetrStruct(# the carrier of PT,FX #) is strict MetrStruct
PT is non empty TopSpace-like TopStruct
the carrier of PT is non empty set
bool the carrier of PT is non empty set
bool (bool the carrier of PT) is non empty set
[: the carrier of PT, the carrier of PT:] is non empty set
[:[: the carrier of PT, the carrier of PT:],REAL:] is set
bool [:[: the carrier of PT, the carrier of PT:],REAL:] is non empty set
R is Relation-like [: the carrier of PT, the carrier of PT:] -defined REAL -valued Function-like V43([: the carrier of PT, the carrier of PT:], REAL ) Element of bool [:[: the carrier of PT, the carrier of PT:],REAL:]
metr is Reflexive discerning symmetric triangle MetrStruct
SpaceMetr ( the carrier of PT,R) is strict Reflexive discerning symmetric triangle MetrStruct
FX is Element of bool (bool the carrier of PT)
the carrier of metr is set
bool the carrier of metr is non empty set
bool (bool the carrier of metr) is non empty set
PT is non empty set
bool PT is non empty Element of bool (bool PT)
bool PT is non empty set
bool (bool PT) is non empty set
bool (bool PT) is non empty Element of bool (bool (bool PT))
bool (bool PT) is non empty set
bool (bool (bool PT)) is non empty set
(bool (bool PT)) * is non empty functional FinSequence-membered M10( bool (bool PT))
[:NAT,((bool (bool PT)) *):] is non empty set
bool [:NAT,((bool (bool PT)) *):] is non empty set
metr is Relation-like NAT -defined (bool (bool PT)) * -valued Function-like V43( NAT ,(bool (bool PT)) * ) Element of bool [:NAT,((bool (bool PT)) *):]
FX is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
metr . FX is FinSequence-like set
metr . FX is FinSequence-like Element of (bool (bool PT)) *
F1() is non empty set
bool F1() is non empty set
bool (bool F1()) is non empty set
bool F1() is non empty Element of bool (bool F1())
bool (bool F1()) is non empty Element of bool (bool (bool F1()))
bool (bool F1()) is non empty set
bool (bool (bool F1())) is non empty set
[:NAT,(bool (bool F1())):] is non empty set
bool [:NAT,(bool (bool F1())):] is non empty set
F2() is Element of bool (bool F1())
(bool (bool F1())) * is non empty functional FinSequence-membered M10( bool (bool F1()))
<*F2()*> is non empty Relation-like NAT -defined bool (bool F1()) -valued Function-like finite V62(1) FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
{ (union { F3(b2,a1) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= a1 or not b3 = a2 /. (b4 + 1) or P2[b2,b1,a1,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } is set
<* { (union { F3(b2,a1) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= a1 or not b3 = a2 /. (b4 + 1) or P2[b2,b1,a1,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } *> is non empty Relation-like NAT -defined Function-like finite V62(1) FinSequence-like FinSubsequence-like set
metr is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
FX is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like Element of (bool (bool F1())) *
{ (union { F3(b2,metr) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= metr or not b3 = FX /. (b4 + 1) or P2[b2,b1,metr,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } is set
<* { (union { F3(b2,metr) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= metr or not b3 = FX /. (b4 + 1) or P2[b2,b1,metr,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } *> is non empty Relation-like NAT -defined Function-like finite V62(1) FinSequence-like FinSubsequence-like set
FX ^ <* { (union { F3(b2,metr) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= metr or not b3 = FX /. (b4 + 1) or P2[b2,b1,metr,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } *> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Mn is set
PM is Element of bool F1()
{ F3(b1,metr) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= metr or not b2 = FX /. (b3 + 1) or P2[b1,PM,metr,b2] ) } is set
union { F3(b1,metr) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= metr or not b2 = FX /. (b3 + 1) or P2[b1,PM,metr,b2] ) } is set
PM is set
UB is set
UB is Element of F1()
F3(UB,metr) is Element of bool F1()
Mn is Element of bool (bool F1())
<*Mn*> is non empty Relation-like NAT -defined bool (bool F1()) -valued Function-like finite V62(1) FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
PM is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
FX ^ PM is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
PM is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
UB is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like Element of (bool (bool F1())) *
[:NAT,((bool (bool F1())) *):] is non empty set
bool [:NAT,((bool (bool F1())) *):] is non empty set
PT is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like Element of (bool (bool F1())) *
metr is Relation-like NAT -defined (bool (bool F1())) * -valued Function-like V43( NAT ,(bool (bool F1())) * ) Element of bool [:NAT,((bool (bool F1())) *):]
(F1(),metr,0) is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
FX is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,FX) is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
len (F1(),metr,FX) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
FX + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,(FX + 1)) is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
len (F1(),metr,(FX + 1)) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(FX + 1) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
{ (union { F3(b2,FX) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= FX or not b3 = (F1(),metr,FX) /. (b4 + 1) or P2[b2,b1,FX,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } is set
<* { (union { F3(b2,FX) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= FX or not b3 = (F1(),metr,FX) /. (b4 + 1) or P2[b2,b1,FX,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } *> is non empty Relation-like NAT -defined Function-like finite V62(1) FinSequence-like FinSubsequence-like set
(F1(),metr,FX) ^ <* { (union { F3(b2,FX) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= FX or not b3 = (F1(),metr,FX) /. (b4 + 1) or P2[b2,b1,FX,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } *> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len ((F1(),metr,FX) ^ <* { (union { F3(b2,FX) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= FX or not b3 = (F1(),metr,FX) /. (b4 + 1) or P2[b2,b1,FX,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } *>) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(len (F1(),metr,FX)) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
FX is Relation-like NAT -defined bool (bool F1()) -valued Function-like V43( NAT , bool (bool F1())) Element of bool [:NAT,(bool (bool F1())):]
FX . 0 is Element of bool (bool F1())
len <*F2()*> is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
<*F2()*> /. 1 is Element of bool (bool F1())
R is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
R + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
FX . (R + 1) is Element of bool (bool F1())
{ (union { F3(b2,R) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= R or not b3 = FX . b4 or P2[b2,b1,R,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } is set
len (F1(),metr,0) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
0 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,R) is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
len (F1(),metr,R) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(len (F1(),metr,R)) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(R + 1) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
Mn is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,Mn) is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
Mn + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,(Mn + 1)) is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
PM is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
FX . PM is Element of bool (bool F1())
PM + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,(Mn + 1)) /. (PM + 1) is Element of bool (bool F1())
(F1(),metr,PM) is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
len (F1(),metr,PM) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,PM) /. (len (F1(),metr,PM)) is Element of bool (bool F1())
Seg (Mn + 1) is non empty V46() V47() V48() V49() V50() V51() finite V62(Mn + 1) Element of bool NAT
len (F1(),metr,Mn) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
Seg (len (F1(),metr,Mn)) is V46() V47() V48() V49() V50() V51() finite V62( len (F1(),metr,Mn)) Element of bool NAT
dom (F1(),metr,Mn) is V46() V47() V48() V49() V50() V51() finite Element of bool NAT
(Mn + 1) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
Seg ((Mn + 1) + 1) is non empty V46() V47() V48() V49() V50() V51() finite V62((Mn + 1) + 1) Element of bool NAT
len (F1(),metr,(Mn + 1)) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
Seg (len (F1(),metr,(Mn + 1))) is V46() V47() V48() V49() V50() V51() finite V62( len (F1(),metr,(Mn + 1))) Element of bool NAT
dom (F1(),metr,(Mn + 1)) is V46() V47() V48() V49() V50() V51() finite Element of bool NAT
(F1(),metr,(Mn + 1)) . (PM + 1) is set
{ (union { F3(b2,Mn) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= Mn or not b3 = (F1(),metr,Mn) /. (b4 + 1) or P2[b2,b1,Mn,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } is set
<* { (union { F3(b2,Mn) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= Mn or not b3 = (F1(),metr,Mn) /. (b4 + 1) or P2[b2,b1,Mn,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } *> is non empty Relation-like NAT -defined Function-like finite V62(1) FinSequence-like FinSubsequence-like set
(F1(),metr,Mn) ^ <* { (union { F3(b2,Mn) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= Mn or not b3 = (F1(),metr,Mn) /. (b4 + 1) or P2[b2,b1,Mn,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } *> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((F1(),metr,Mn) ^ <* { (union { F3(b2,Mn) where b2 is Element of F1() : for b3 being Element of bool (bool F1())
for b4 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b4 <= Mn or not b3 = (F1(),metr,Mn) /. (b4 + 1) or P2[b2,b1,Mn,b3] ) } ) where b1 is Element of bool F1() : P1[b1] } *>) . (PM + 1) is set
(F1(),metr,Mn) . (PM + 1) is set
(F1(),metr,Mn) /. (PM + 1) is Element of bool (bool F1())
{ F3(b1,R) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= R or not b2 = (F1(),metr,R) /. (b3 + 1) or P2[b1,a1,R,b2] ) } is set
union { F3(b1,R) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= R or not b2 = (F1(),metr,R) /. (b3 + 1) or P2[b1,a1,R,b2] ) } is set
{ F3(b1,R) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= R or not b2 = FX . b3 or P2[b1,a1,R,b2] ) } is set
union { F3(b1,R) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= R or not b2 = FX . b3 or P2[b1,a1,R,b2] ) } is set
{ H3(b1) where b1 is Element of bool F1() : P1[b1] } is set
(F1(),metr,(R + 1)) is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
len (F1(),metr,(R + 1)) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
dom (F1(),metr,(R + 1)) is V46() V47() V48() V49() V50() V51() finite Element of bool NAT
Seg ((R + 1) + 1) is non empty V46() V47() V48() V49() V50() V51() finite V62((R + 1) + 1) Element of bool NAT
PM is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
FX . PM is Element of bool (bool F1())
PM + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,0) /. (PM + 1) is Element of bool (bool F1())
(F1(),metr,PM) is Relation-like NAT -defined bool (bool F1()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool F1())
len (F1(),metr,PM) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,PM) /. (len (F1(),metr,PM)) is Element of bool (bool F1())
PM is Element of bool F1()
{ F3(b1,R) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= R or not b2 = FX . b3 or P2[b1,PM,R,b2] ) } is set
union { F3(b1,R) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= R or not b2 = FX . b3 or P2[b1,PM,R,b2] ) } is set
{ F3(b1,R) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= R or not b2 = (F1(),metr,R) /. (b3 + 1) or P2[b1,PM,R,b2] ) } is set
union { F3(b1,R) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= R or not b2 = (F1(),metr,R) /. (b3 + 1) or P2[b1,PM,R,b2] ) } is set
PM is Element of F1()
UB is Element of bool (bool F1())
UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
UB + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,R) /. (UB + 1) is Element of bool (bool F1())
FX . UB is Element of bool (bool F1())
UB is Element of bool (bool F1())
UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
FX . UB is Element of bool (bool F1())
UB + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,R) /. (UB + 1) is Element of bool (bool F1())
{ H4(b1) where b1 is Element of F1() : S4[b1] } is set
{ H4(b1) where b1 is Element of F1() : S5[b1] } is set
{ H2(b1) where b1 is Element of bool F1() : P1[b1] } is set
<* { H3(b1) where b1 is Element of bool F1() : P1[b1] } *> is non empty Relation-like NAT -defined Function-like finite V62(1) FinSequence-like FinSubsequence-like set
(F1(),metr,R) ^ <* { H3(b1) where b1 is Element of bool F1() : P1[b1] } *> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len ((F1(),metr,R) ^ <* { H3(b1) where b1 is Element of bool F1() : P1[b1] } *>) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(F1(),metr,(R + 1)) /. ((len (F1(),metr,R)) + 1) is Element of bool (bool F1())
(F1(),metr,(R + 1)) . ((len (F1(),metr,R)) + 1) is set
((F1(),metr,R) ^ <* { H3(b1) where b1 is Element of bool F1() : P1[b1] } *>) . ((len (F1(),metr,R)) + 1) is set
F1() is non empty set
bool F1() is non empty set
bool (bool F1()) is non empty set
bool F1() is non empty Element of bool (bool F1())
bool (bool F1()) is non empty Element of bool (bool (bool F1()))
bool (bool F1()) is non empty set
bool (bool (bool F1())) is non empty set
[:NAT,(bool (bool F1())):] is non empty set
bool [:NAT,(bool (bool F1())):] is non empty set
F2() is Element of bool (bool F1())
PT is Relation-like NAT -defined bool (bool F1()) -valued Function-like V43( NAT , bool (bool F1())) Element of bool [:NAT,(bool (bool F1())):]
PT . 0 is Element of bool (bool F1())
metr is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
metr + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
PT . (metr + 1) is Element of bool (bool F1())
{ (union (PT . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= metr } is set
union { (union (PT . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= metr } is set
{ (union { F3(b2,metr) where b2 is Element of F1() : ( P2[b2,b1,metr] & not b2 in union { (union (PT . b1)) where b3 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= metr } ) } ) where b1 is Element of bool F1() : P1[b1] } is set
{ F3(b1,metr) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= metr or not b2 = PT . b3 or ( P2[b1,a1,metr] & not b1 in union b2 ) ) } is set
union { F3(b1,metr) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= metr or not b2 = PT . b3 or ( P2[b1,a1,metr] & not b1 in union b2 ) ) } is set
{ F3(b1,metr) where b1 is Element of F1() : ( P2[b1,a1,metr] & not b1 in union { (union (PT . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= metr } ) } is set
union { F3(b1,metr) where b1 is Element of F1() : ( P2[b1,a1,metr] & not b1 in union { (union (PT . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= metr } ) } is set
{ H1(b1) where b1 is Element of bool F1() : P1[b1] } is set
{ H2(b1) where b1 is Element of bool F1() : P1[b1] } is set
Mn is Element of bool F1()
PM is Element of F1()
PM is set
UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
PT . UB is Element of bool (bool F1())
union (PT . UB) is Element of bool F1()
PM is Element of bool (bool F1())
union PM is Element of bool F1()
UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
PT . UB is Element of bool (bool F1())
PM is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
PT . PM is Element of bool (bool F1())
UB is Element of bool (bool F1())
UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
UB is Element of bool (bool F1())
PT . UB is Element of bool (bool F1())
union UB is Element of bool F1()
UB is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
PM is Element of bool (bool F1())
PT . UB is Element of bool (bool F1())
union PM is Element of bool F1()
f is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
UB is Element of bool (bool F1())
PT . f is Element of bool (bool F1())
union UB is Element of bool F1()
{ H3(b1) where b1 is Element of F1() : S2[b1] } is set
{ H3(b1) where b1 is Element of F1() : S3[b1] } is set
{ F3(b1,metr) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= metr or not b2 = PT . b3 or ( P2[b1,Mn,metr] & not b1 in union b2 ) ) } is set
union { F3(b1,metr) where b1 is Element of F1() : for b2 being Element of bool (bool F1())
for b3 being V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT holds
( not b3 <= metr or not b2 = PT . b3 or ( P2[b1,Mn,metr] & not b1 in union b2 ) ) } is set
{ F3(b1,metr) where b1 is Element of F1() : ( P2[b1,Mn,metr] & not b1 in union { (union (PT . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= metr } ) } is set
union { F3(b1,metr) where b1 is Element of F1() : ( P2[b1,Mn,metr] & not b1 in union { (union (PT . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= metr } ) } is set
PT is non empty TopSpace-like TopStruct
the carrier of PT is non empty set
bool the carrier of PT is non empty set
bool (bool the carrier of PT) is non empty set
[: the carrier of PT, the carrier of PT:] is non empty set
[:[: the carrier of PT, the carrier of PT:],REAL:] is set
bool [:[: the carrier of PT, the carrier of PT:],REAL:] is non empty set
the topology of PT is non empty Element of bool (bool the carrier of PT)
metr is Relation-like [: the carrier of PT, the carrier of PT:] -defined REAL -valued Function-like V43([: the carrier of PT, the carrier of PT:], REAL ) Element of bool [:[: the carrier of PT, the carrier of PT:],REAL:]
SpaceMetr ( the carrier of PT,metr) is strict Reflexive discerning symmetric triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of PT,metr)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of PT,metr)))
the carrier of (SpaceMetr ( the carrier of PT,metr)) is set
bool the carrier of (SpaceMetr ( the carrier of PT,metr)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of PT,metr))) is non empty set
FX is Element of bool (bool the carrier of PT)
R is Relation-like set
R |_2 FX is Relation-like set
[:FX,FX:] is set
R /\ [:FX,FX:] is set
Mn is Relation-like set
PM is Reflexive discerning symmetric triangle MetrStruct
PM is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of PM is non empty set
bool the carrier of PM is non empty set
1 / 2 is V34() V35() ext-real Element of REAL
3 / 2 is V34() V35() ext-real Element of REAL
{ (union { (Ball (b2,(1 / 2))) where b2 is Element of the carrier of PM : ( b2 in b1 \ ((bool the carrier of PM),Mn,b1) & Ball (b2,(3 / 2)) c= b1 ) } ) where b1 is Element of bool the carrier of PM : b1 in FX } is set
bool (bool the carrier of PM) is non empty set
UB is set
bool the carrier of PM is non empty Element of bool (bool the carrier of PM)
f is set
GX is Element of bool the carrier of PM
((bool the carrier of PM),Mn,GX) is set
Mn -Seg GX is set
Coim (Mn,GX) is set
{GX} is finite set
(Coim (Mn,GX)) \ {GX} is Element of bool (Coim (Mn,GX))
bool (Coim (Mn,GX)) is non empty set
union (Mn -Seg GX) is set
GX \ ((bool the carrier of PM),Mn,GX) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in GX \ ((bool the carrier of PM),Mn,GX) & Ball (b1,(3 / 2)) c= GX ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in GX \ ((bool the carrier of PM),Mn,GX) & Ball (b1,(3 / 2)) c= GX ) } is set
GX is set
x is set
x9 is Element of the carrier of PM
Ball (x9,(1 / 2)) is Element of bool the carrier of PM
Ball (x9,(3 / 2)) is Element of bool the carrier of PM
bool the carrier of PM is non empty Element of bool (bool the carrier of PM)
bool (bool the carrier of PM) is non empty Element of bool (bool (bool the carrier of PM))
bool (bool the carrier of PM) is non empty set
bool (bool (bool the carrier of PM)) is non empty set
[:NAT,(bool (bool the carrier of PM)):] is non empty set
bool [:NAT,(bool (bool the carrier of PM)):] is non empty set
UB is Element of bool (bool the carrier of PM)
f is Relation-like NAT -defined bool (bool the carrier of PM) -valued Function-like V43( NAT , bool (bool the carrier of PM)) Element of bool [:NAT,(bool (bool the carrier of PM)):]
f . 0 is Element of bool (bool the carrier of PM)
GX is Element of bool (bool the carrier of PM)
GX is Element of bool (bool the carrier of PT)
x is Element of bool the carrier of PT
x9 is Element of bool the carrier of PM
X is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . X is Element of bool (bool the carrier of PM)
X is Element of bool the carrier of PM
((bool the carrier of PM),Mn,X) is set
Mn -Seg X is set
Coim (Mn,X) is set
{X} is finite set
(Coim (Mn,X)) \ {X} is Element of bool (Coim (Mn,X))
bool (Coim (Mn,X)) is non empty set
union (Mn -Seg X) is set
X \ ((bool the carrier of PM),Mn,X) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in X \ ((bool the carrier of PM),Mn,X) & Ball (b1,(3 / 2)) c= X ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in X \ ((bool the carrier of PM),Mn,X) & Ball (b1,(3 / 2)) c= X ) } is set
m is set
k is Element of the carrier of PM
Ball (k,(1 / 2)) is Element of bool the carrier of PM
Ball (k,(3 / 2)) is Element of bool the carrier of PM
m is Element of bool (bool the carrier of PM)
Family_open_set PM is Element of bool (bool the carrier of PM)
k is set
W is Element of the carrier of PM
Ball (W,(1 / 2)) is Element of bool the carrier of PM
Ball (W,(3 / 2)) is Element of bool the carrier of PM
X is V27() V28() V29() V33() ext-real non negative set
X + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
r is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
r + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ (r + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 / (2 |^ (r + 1)) is V34() V35() ext-real Element of REAL
3 / (2 |^ (r + 1)) is V34() V35() ext-real Element of REAL
{ (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } is set
union { (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } is set
{ (union { (Ball (b2,(1 / (2 |^ (r + 1))))) where b2 is Element of the carrier of PM : ( b2 in b1 \ ((bool the carrier of PM),Mn,b1) & Ball (b2,(3 / (2 |^ (r + 1)))) c= b1 & not b2 in union { (union (f . b1)) where b3 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } ) } ) where b1 is Element of bool the carrier of PM : b1 in FX } is set
m is Element of bool the carrier of PM
((bool the carrier of PM),Mn,m) is set
Mn -Seg m is set
Coim (Mn,m) is set
{m} is finite set
(Coim (Mn,m)) \ {m} is Element of bool (Coim (Mn,m))
bool (Coim (Mn,m)) is non empty set
union (Mn -Seg m) is set
m \ ((bool the carrier of PM),Mn,m) is Element of bool the carrier of PM
{ (Ball (b1,(1 / (2 |^ (r + 1))))) where b1 is Element of the carrier of PM : ( b1 in m \ ((bool the carrier of PM),Mn,m) & Ball (b1,(3 / (2 |^ (r + 1)))) c= m & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } ) } is set
union { (Ball (b1,(1 / (2 |^ (r + 1))))) where b1 is Element of the carrier of PM : ( b1 in m \ ((bool the carrier of PM),Mn,m) & Ball (b1,(3 / (2 |^ (r + 1)))) c= m & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } ) } is set
k is set
W is set
W is Element of the carrier of PM
Ball (W,(1 / (2 |^ (r + 1)))) is Element of bool the carrier of PM
Ball (W,(3 / (2 |^ (r + 1)))) is Element of bool the carrier of PM
W is Element of bool (bool the carrier of PM)
Family_open_set PM is Element of bool (bool the carrier of PM)
W is set
NZ is Element of the carrier of PM
Ball (NZ,(1 / (2 |^ (r + 1)))) is Element of bool the carrier of PM
Ball (NZ,(3 / (2 |^ (r + 1)))) is Element of bool the carrier of PM
union GX is Element of bool the carrier of PT
x is set
X is Element of bool the carrier of PT
X is set
X is Element of bool the carrier of PT
Family_open_set PM is Element of bool (bool the carrier of PM)
x9 is Element of the carrier of PM
r is Element of bool the carrier of PM
m is V34() V35() ext-real Element of REAL
Ball (x9,m) is Element of bool the carrier of PM
k is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ k is V34() V35() ext-real Element of REAL
3 / (2 |^ k) is V34() V35() ext-real Element of REAL
k is V27() V28() V29() V33() ext-real non negative set
2 |^ k is V34() V35() ext-real Element of REAL
3 / (2 |^ k) is V34() V35() ext-real Element of REAL
k + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ (k + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(2 |^ k) * 2 is V34() V35() ext-real Element of REAL
3 / (2 |^ (k + 1)) is V34() V35() ext-real Element of REAL
W is set
W is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . W is Element of bool (bool the carrier of PM)
W is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . W is Element of bool (bool the carrier of PM)
union (f . W) is Element of bool the carrier of PM
W is set
1 / (2 |^ (k + 1)) is V34() V35() ext-real Element of REAL
((bool the carrier of PM),Mn,r) is set
Mn -Seg r is set
Coim (Mn,r) is set
{r} is finite set
(Coim (Mn,r)) \ {r} is Element of bool (Coim (Mn,r))
bool (Coim (Mn,r)) is non empty set
union (Mn -Seg r) is set
r \ ((bool the carrier of PM),Mn,r) is Element of bool the carrier of PM
{ (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= k } is set
union { (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= k } is set
{ (Ball (b1,(1 / (2 |^ (k + 1))))) where b1 is Element of the carrier of PM : ( b1 in r \ ((bool the carrier of PM),Mn,r) & Ball (b1,(3 / (2 |^ (k + 1)))) c= r & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= k } ) } is set
union { (Ball (b1,(1 / (2 |^ (k + 1))))) where b1 is Element of the carrier of PM : ( b1 in r \ ((bool the carrier of PM),Mn,r) & Ball (b1,(3 / (2 |^ (k + 1)))) c= r & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= k } ) } is set
W is set
NZ is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . NZ is Element of bool (bool the carrier of PM)
union (f . NZ) is Element of bool the carrier of PM
NZ is set
W is set
[NZ,r] is set
{NZ,r} is finite set
{NZ} is finite set
{{NZ,r},{NZ}} is finite V59() set
field Mn is set
[r,NZ] is set
{r,NZ} is finite set
{{r,NZ},{r}} is finite V59() set
Ball (x9,(1 / (2 |^ (k + 1)))) is Element of bool the carrier of PM
W is Element of bool the carrier of PM
Ball (x9,(3 / (2 |^ (k + 1)))) is Element of bool the carrier of PM
W is set
{ (union { (Ball (b2,(1 / (2 |^ (k + 1))))) where b2 is Element of the carrier of PM : ( b2 in b1 \ ((bool the carrier of PM),Mn,b1) & Ball (b2,(3 / (2 |^ (k + 1)))) c= b1 & not b2 in union { (union (f . b1)) where b3 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= k } ) } ) where b1 is Element of bool the carrier of PM : b1 in FX } is set
f . (k + 1) is Element of bool (bool the carrier of PM)
W is set
W is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . W is Element of bool (bool the carrier of PM)
x is set
x9 is Element of bool the carrier of PM
X is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . X is Element of bool (bool the carrier of PM)
X is Element of bool the carrier of PM
((bool the carrier of PM),Mn,X) is set
Mn -Seg X is set
Coim (Mn,X) is set
{X} is finite set
(Coim (Mn,X)) \ {X} is Element of bool (Coim (Mn,X))
bool (Coim (Mn,X)) is non empty set
union (Mn -Seg X) is set
X \ ((bool the carrier of PM),Mn,X) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in X \ ((bool the carrier of PM),Mn,X) & Ball (b1,(3 / 2)) c= X ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in X \ ((bool the carrier of PM),Mn,X) & Ball (b1,(3 / 2)) c= X ) } is set
m is set
k is Element of the carrier of PM
Ball (k,(1 / 2)) is Element of bool the carrier of PM
Ball (k,(3 / 2)) is Element of bool the carrier of PM
m is Element of bool (bool the carrier of PM)
k is set
W is Element of the carrier of PM
Ball (W,(1 / 2)) is Element of bool the carrier of PM
Ball (W,(3 / 2)) is Element of bool the carrier of PM
k is set
W is set
X is V27() V28() V29() V33() ext-real non negative set
X + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
r is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
r + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ (r + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 / (2 |^ (r + 1)) is V34() V35() ext-real Element of REAL
3 / (2 |^ (r + 1)) is V34() V35() ext-real Element of REAL
{ (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } is set
union { (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } is set
{ (union { (Ball (b2,(1 / (2 |^ (r + 1))))) where b2 is Element of the carrier of PM : ( b2 in b1 \ ((bool the carrier of PM),Mn,b1) & Ball (b2,(3 / (2 |^ (r + 1)))) c= b1 & not b2 in union { (union (f . b1)) where b3 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } ) } ) where b1 is Element of bool the carrier of PM : b1 in FX } is set
m is Element of bool the carrier of PM
((bool the carrier of PM),Mn,m) is set
Mn -Seg m is set
Coim (Mn,m) is set
{m} is finite set
(Coim (Mn,m)) \ {m} is Element of bool (Coim (Mn,m))
bool (Coim (Mn,m)) is non empty set
union (Mn -Seg m) is set
m \ ((bool the carrier of PM),Mn,m) is Element of bool the carrier of PM
{ (Ball (b1,(1 / (2 |^ (r + 1))))) where b1 is Element of the carrier of PM : ( b1 in m \ ((bool the carrier of PM),Mn,m) & Ball (b1,(3 / (2 |^ (r + 1)))) c= m & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } ) } is set
union { (Ball (b1,(1 / (2 |^ (r + 1))))) where b1 is Element of the carrier of PM : ( b1 in m \ ((bool the carrier of PM),Mn,m) & Ball (b1,(3 / (2 |^ (r + 1)))) c= m & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= r } ) } is set
k is set
W is set
W is Element of the carrier of PM
Ball (W,(1 / (2 |^ (r + 1)))) is Element of bool the carrier of PM
Ball (W,(3 / (2 |^ (r + 1)))) is Element of bool the carrier of PM
W is Element of bool (bool the carrier of PM)
W is set
NZ is Element of the carrier of PM
Ball (NZ,(1 / (2 |^ (r + 1)))) is Element of bool the carrier of PM
Ball (NZ,(3 / (2 |^ (r + 1)))) is Element of bool the carrier of PM
W is set
NZ is set
X is set
x is Element of the carrier of PT
X is Element of bool the carrier of PT
X is Element of bool the carrier of PT
Family_open_set PM is Element of bool (bool the carrier of PM)
x9 is Element of the carrier of PM
r is V34() V35() ext-real Element of REAL
Ball (x9,r) is Element of bool the carrier of PM
m is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ m is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 / (2 |^ m) is V34() V35() ext-real Element of REAL
k is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . k is set
k is V27() V28() V29() V33() ext-real non negative set
f . k is set
m + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(m + 1) + k is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
((m + 1) + k) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ (((m + 1) + k) + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 / (2 |^ (((m + 1) + k) + 1)) is V34() V35() ext-real Element of REAL
Ball (x9,(1 / (2 |^ (((m + 1) + k) + 1)))) is Element of bool the carrier of PM
W is Element of bool the carrier of PM
W is Element of bool the carrier of PT
{ b1 where b1 is Element of bool the carrier of PT : ( b1 in GX & not b1 misses W ) } is set
g is set
x is Element of bool the carrier of PT
g is Relation-like Function-like set
dom g is set
rng g is set
{ b1 where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : not ((m + 1) + k) + 1 <= b1 } is set
x is set
x1 is set
g . x1 is set
n1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . n1 is Element of bool (bool the carrier of PM)
n1 is Element of bool the carrier of PT
w1 is set
w2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
w1 is V27() V28() V29() V33() ext-real non negative set
w1 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
w2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
w2 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ (w2 + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 / (2 |^ (w2 + 1)) is V34() V35() ext-real Element of REAL
3 / (2 |^ (w2 + 1)) is V34() V35() ext-real Element of REAL
{ (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= w2 } is set
union { (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= w2 } is set
{ (union { (Ball (b2,(1 / (2 |^ (w2 + 1))))) where b2 is Element of the carrier of PM : ( b2 in b1 \ ((bool the carrier of PM),Mn,b1) & Ball (b2,(3 / (2 |^ (w2 + 1)))) c= b1 & not b2 in union { (union (f . b1)) where b3 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= w2 } ) } ) where b1 is Element of bool the carrier of PM : b1 in FX } is set
l is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . l is Element of bool (bool the carrier of PM)
2 |^ w2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 / (2 |^ w2) is V34() V35() ext-real Element of REAL
l is Element of bool the carrier of PM
((bool the carrier of PM),Mn,l) is set
Mn -Seg l is set
Coim (Mn,l) is set
{l} is finite set
(Coim (Mn,l)) \ {l} is Element of bool (Coim (Mn,l))
bool (Coim (Mn,l)) is non empty set
union (Mn -Seg l) is set
l \ ((bool the carrier of PM),Mn,l) is Element of bool the carrier of PM
{ (Ball (b1,(1 / (2 |^ (w2 + 1))))) where b1 is Element of the carrier of PM : ( b1 in l \ ((bool the carrier of PM),Mn,l) & Ball (b1,(3 / (2 |^ (w2 + 1)))) c= l & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= w2 } ) } is set
union { (Ball (b1,(1 / (2 |^ (w2 + 1))))) where b1 is Element of the carrier of PM : ( b1 in l \ ((bool the carrier of PM),Mn,l) & Ball (b1,(3 / (2 |^ (w2 + 1)))) c= l & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= w2 } ) } is set
l is set
h is set
M1 is Element of the carrier of PM
Ball (M1,(1 / (2 |^ (w2 + 1)))) is Element of bool the carrier of PM
Ball (M1,(3 / (2 |^ (w2 + 1)))) is Element of bool the carrier of PM
i is Element of the carrier of PM
dist (M1,i) is V34() V35() ext-real Element of REAL
dist (i,x9) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + (dist (i,x9)) is V34() V35() ext-real Element of REAL
(dist (M1,i)) + (dist (i,x9)) is V34() V35() ext-real Element of REAL
NF is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . NF is Element of bool (bool the carrier of PM)
union (f . NF) is Element of bool the carrier of PM
dist (M1,x9) is V34() V35() ext-real Element of REAL
dist (x9,M1) is V34() V35() ext-real Element of REAL
f . k is Element of bool (bool the carrier of PM)
union (f . k) is Element of bool the carrier of PM
k + (m + 1) is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(1 / (2 |^ m)) - (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
1 + k is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ (1 + k) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(2 |^ (1 + k)) * 2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 - 1 is V34() V35() ext-real Element of REAL
((2 |^ (1 + k)) * 2) - 1 is V34() V35() ext-real Element of REAL
(1 + k) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ ((1 + k) + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 * (2 |^ ((1 + k) + 1)) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(2 |^ m) * (2 |^ ((1 + k) + 1)) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(1 * (2 |^ ((1 + k) + 1))) / ((2 |^ m) * (2 |^ ((1 + k) + 1))) is V34() V35() ext-real Element of REAL
((1 * (2 |^ ((1 + k) + 1))) / ((2 |^ m) * (2 |^ ((1 + k) + 1)))) - (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
m + ((1 + k) + 1) is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ (m + ((1 + k) + 1)) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(1 * (2 |^ ((1 + k) + 1))) / (2 |^ (m + ((1 + k) + 1))) is V34() V35() ext-real Element of REAL
((1 * (2 |^ ((1 + k) + 1))) / (2 |^ (m + ((1 + k) + 1)))) - (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
((2 |^ (1 + k)) * 2) / (2 |^ (((m + 1) + k) + 1)) is V34() V35() ext-real Element of REAL
(((2 |^ (1 + k)) * 2) / (2 |^ (((m + 1) + k) + 1))) - (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
(((2 |^ (1 + k)) * 2) - 1) / (2 |^ (((m + 1) + k) + 1)) is V34() V35() ext-real Element of REAL
x is set
x1 is set
g . x is set
g . x1 is set
w2 is Element of bool the carrier of PT
w2 is set
n1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . n1 is Element of bool (bool the carrier of PM)
w1 is Element of bool the carrier of PT
w1 is set
m + k is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(m + k) + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ 1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ ((m + 1) + k) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 / (2 |^ ((m + 1) + k)) is V34() V35() ext-real Element of REAL
2 / (2 |^ (((m + 1) + k) + 1)) is V34() V35() ext-real Element of REAL
1 * 2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(2 |^ ((m + 1) + k)) * 2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(1 * 2) / ((2 |^ ((m + 1) + k)) * 2) is V34() V35() ext-real Element of REAL
(1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2) is V34() V35() ext-real Element of REAL
((1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)) is V34() V35() ext-real Element of REAL
1 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(1 + 1) / 2 is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
((1 + 1) / 2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) is V34() V35() ext-real Element of REAL
2 / 2 is V34() V35() ext-real Element of REAL
(2 / 2) + (2 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
(((1 / 2) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) - (2 / 2) is V34() V35() ext-real Element of REAL
(2 / 2) + (1 / 2) is V34() V35() ext-real Element of REAL
w2 is Element of the carrier of PM
dist (x9,w2) is V34() V35() ext-real Element of REAL
l is Element of bool the carrier of PM
((bool the carrier of PM),Mn,l) is set
Mn -Seg l is set
Coim (Mn,l) is set
{l} is finite set
(Coim (Mn,l)) \ {l} is Element of bool (Coim (Mn,l))
bool (Coim (Mn,l)) is non empty set
union (Mn -Seg l) is set
l \ ((bool the carrier of PM),Mn,l) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in l \ ((bool the carrier of PM),Mn,l) & Ball (b1,(3 / 2)) c= l ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in l \ ((bool the carrier of PM),Mn,l) & Ball (b1,(3 / 2)) c= l ) } is set
w1 is Element of the carrier of PM
l is set
h is Element of the carrier of PM
Ball (h,(1 / 2)) is Element of bool the carrier of PM
Ball (h,(3 / 2)) is Element of bool the carrier of PM
dist (h,w1) is V34() V35() ext-real Element of REAL
i is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . i is Element of bool (bool the carrier of PM)
i is Element of bool the carrier of PM
((bool the carrier of PM),Mn,i) is set
Mn -Seg i is set
Coim (Mn,i) is set
{i} is finite set
(Coim (Mn,i)) \ {i} is Element of bool (Coim (Mn,i))
bool (Coim (Mn,i)) is non empty set
union (Mn -Seg i) is set
i \ ((bool the carrier of PM),Mn,i) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in i \ ((bool the carrier of PM),Mn,i) & Ball (b1,(3 / 2)) c= i ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in i \ ((bool the carrier of PM),Mn,i) & Ball (b1,(3 / 2)) c= i ) } is set
M1 is set
NF is Element of the carrier of PM
Ball (NF,(1 / 2)) is Element of bool the carrier of PM
Ball (NF,(3 / 2)) is Element of bool the carrier of PM
dist (x9,NF) is V34() V35() ext-real Element of REAL
dist (w2,NF) is V34() V35() ext-real Element of REAL
(dist (x9,w2)) + (dist (w2,NF)) is V34() V35() ext-real Element of REAL
dist (h,x9) is V34() V35() ext-real Element of REAL
dist (w1,x9) is V34() V35() ext-real Element of REAL
(dist (h,w1)) + (dist (w1,x9)) is V34() V35() ext-real Element of REAL
(dist (h,x9)) + (dist (x9,NF)) is V34() V35() ext-real Element of REAL
((dist (h,w1)) + (dist (w1,x9))) + ((dist (x9,w2)) + (dist (w2,NF))) is V34() V35() ext-real Element of REAL
dist (h,NF) is V34() V35() ext-real Element of REAL
(dist (w1,x9)) + ((dist (x9,w2)) + (dist (w2,NF))) is V34() V35() ext-real Element of REAL
(dist (h,w1)) + ((dist (w1,x9)) + ((dist (x9,w2)) + (dist (w2,NF)))) is V34() V35() ext-real Element of REAL
(dist (h,NF)) - ((dist (w1,x9)) + ((dist (x9,w2)) + (dist (w2,NF)))) is V34() V35() ext-real Element of REAL
(1 / 2) + ((dist (w1,x9)) + ((dist (x9,w2)) + (dist (w2,NF)))) is V34() V35() ext-real Element of REAL
(1 / 2) + ((dist (x9,w2)) + (dist (w2,NF))) is V34() V35() ext-real Element of REAL
(dist (w1,x9)) + ((1 / 2) + ((dist (x9,w2)) + (dist (w2,NF)))) is V34() V35() ext-real Element of REAL
(dist (h,NF)) - ((1 / 2) + ((dist (x9,w2)) + (dist (w2,NF)))) is V34() V35() ext-real Element of REAL
dist (x9,w1) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / 2) + ((dist (x9,w2)) + (dist (w2,NF)))) is V34() V35() ext-real Element of REAL
(dist (w2,NF)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)) is V34() V35() ext-real Element of REAL
(dist (x9,w2)) + ((dist (w2,NF)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) is V34() V35() ext-real Element of REAL
(dist (h,NF)) - ((dist (w2,NF)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + ((dist (w2,NF)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2)) is V34() V35() ext-real Element of REAL
(dist (w2,NF)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) is V34() V35() ext-real Element of REAL
(dist (h,NF)) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) is V34() V35() ext-real Element of REAL
dist (NF,w2) is V34() V35() ext-real Element of REAL
(1 / 2) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / 2))) is V34() V35() ext-real Element of REAL
[l,i] is set
{l,i} is finite set
{{l,i},{l}} is finite V59() set
[i,l] is set
{i,l} is finite set
{{i,l},{i}} is finite V59() set
[l,i] is set
{l,i} is finite set
{{l,i},{l}} is finite V59() set
[i,l] is set
{i,l} is finite set
{{i,l},{i}} is finite V59() set
l is V27() V28() V29() V33() ext-real non negative set
l + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
l is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
l + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ (l + 1) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 / (2 |^ (l + 1)) is V34() V35() ext-real Element of REAL
3 / (2 |^ (l + 1)) is V34() V35() ext-real Element of REAL
{ (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= l } is set
union { (union (f . b1)) where b1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= l } is set
{ (union { (Ball (b2,(1 / (2 |^ (l + 1))))) where b2 is Element of the carrier of PM : ( b2 in b1 \ ((bool the carrier of PM),Mn,b1) & Ball (b2,(3 / (2 |^ (l + 1)))) c= b1 & not b2 in union { (union (f . b1)) where b3 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= l } ) } ) where b1 is Element of bool the carrier of PM : b1 in FX } is set
w2 is Element of the carrier of PM
dist (x9,w2) is V34() V35() ext-real Element of REAL
h is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
f . h is Element of bool (bool the carrier of PM)
(1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))) is V34() V35() ext-real Element of REAL
((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (l + 1))) + (1 / (2 |^ (l + 1))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
((1 / (2 |^ (l + 1))) + (1 / (2 |^ (l + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) is V34() V35() ext-real Element of REAL
1 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(1 + 1) / (2 |^ (l + 1)) is V34() V35() ext-real Element of REAL
((1 + 1) / (2 |^ (l + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) is V34() V35() ext-real Element of REAL
2 / (2 |^ (l + 1)) is V34() V35() ext-real Element of REAL
2 / (2 |^ (((m + 1) + k) + 1)) is V34() V35() ext-real Element of REAL
(2 / (2 |^ (l + 1))) + (2 / (2 |^ (((m + 1) + k) + 1))) is V34() V35() ext-real Element of REAL
h is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
h is V27() V28() V29() V33() ext-real non negative set
(l + 1) + h is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
i is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
i is V27() V28() V29() V33() ext-real non negative set
i + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(l + 1) + i is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
2 |^ ((l + 1) + i) is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
1 / (2 |^ ((l + 1) + i)) is V34() V35() ext-real Element of REAL
1 * 2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(2 |^ ((l + 1) + i)) * 2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(1 * 2) / ((2 |^ ((l + 1) + i)) * 2) is V34() V35() ext-real Element of REAL
(((1 / (2 |^ (l + 1))) + (1 / (2 |^ (((m + 1) + k) + 1)))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) - (2 / (2 |^ (l + 1))) is V34() V35() ext-real Element of REAL
(2 / (2 |^ (l + 1))) + (1 / (2 |^ (l + 1))) is V34() V35() ext-real Element of REAL
2 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
(2 + 1) / (2 |^ (l + 1)) is V34() V35() ext-real Element of REAL
M1 is Element of bool the carrier of PM
((bool the carrier of PM),Mn,M1) is set
Mn -Seg M1 is set
Coim (Mn,M1) is set
{M1} is finite set
(Coim (Mn,M1)) \ {M1} is Element of bool (Coim (Mn,M1))
bool (Coim (Mn,M1)) is non empty set
union (Mn -Seg M1) is set
M1 \ ((bool the carrier of PM),Mn,M1) is Element of bool the carrier of PM
{ (Ball (b1,(1 / (2 |^ (l + 1))))) where b1 is Element of the carrier of PM : ( b1 in M1 \ ((bool the carrier of PM),Mn,M1) & Ball (b1,(3 / (2 |^ (l + 1)))) c= M1 & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= l } ) } is set
union { (Ball (b1,(1 / (2 |^ (l + 1))))) where b1 is Element of the carrier of PM : ( b1 in M1 \ ((bool the carrier of PM),Mn,M1) & Ball (b1,(3 / (2 |^ (l + 1)))) c= M1 & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= l } ) } is set
w1 is Element of the carrier of PM
NF is set
k1 is set
c1 is Element of the carrier of PM
Ball (c1,(1 / (2 |^ (l + 1)))) is Element of bool the carrier of PM
Ball (c1,(3 / (2 |^ (l + 1)))) is Element of bool the carrier of PM
dist (c1,w1) is V34() V35() ext-real Element of REAL
M2 is Element of bool the carrier of PM
((bool the carrier of PM),Mn,M2) is set
Mn -Seg M2 is set
Coim (Mn,M2) is set
{M2} is finite set
(Coim (Mn,M2)) \ {M2} is Element of bool (Coim (Mn,M2))
bool (Coim (Mn,M2)) is non empty set
union (Mn -Seg M2) is set
M2 \ ((bool the carrier of PM),Mn,M2) is Element of bool the carrier of PM
{ (Ball (b1,(1 / (2 |^ (l + 1))))) where b1 is Element of the carrier of PM : ( b1 in M2 \ ((bool the carrier of PM),Mn,M2) & Ball (b1,(3 / (2 |^ (l + 1)))) c= M2 & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= l } ) } is set
union { (Ball (b1,(1 / (2 |^ (l + 1))))) where b1 is Element of the carrier of PM : ( b1 in M2 \ ((bool the carrier of PM),Mn,M2) & Ball (b1,(3 / (2 |^ (l + 1)))) c= M2 & not b1 in union { (union (f . b1)) where b2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT : b1 <= l } ) } is set
NF is set
k2 is set
c2 is Element of the carrier of PM
Ball (c2,(1 / (2 |^ (l + 1)))) is Element of bool the carrier of PM
Ball (c2,(3 / (2 |^ (l + 1)))) is Element of bool the carrier of PM
dist (x9,c2) is V34() V35() ext-real Element of REAL
dist (w2,c2) is V34() V35() ext-real Element of REAL
(dist (x9,w2)) + (dist (w2,c2)) is V34() V35() ext-real Element of REAL
dist (c1,x9) is V34() V35() ext-real Element of REAL
dist (w1,x9) is V34() V35() ext-real Element of REAL
(dist (c1,w1)) + (dist (w1,x9)) is V34() V35() ext-real Element of REAL
(dist (c1,x9)) + (dist (x9,c2)) is V34() V35() ext-real Element of REAL
((dist (c1,w1)) + (dist (w1,x9))) + ((dist (x9,w2)) + (dist (w2,c2))) is V34() V35() ext-real Element of REAL
dist (c1,c2) is V34() V35() ext-real Element of REAL
(dist (w1,x9)) + ((dist (x9,w2)) + (dist (w2,c2))) is V34() V35() ext-real Element of REAL
(dist (c1,w1)) + ((dist (w1,x9)) + ((dist (x9,w2)) + (dist (w2,c2)))) is V34() V35() ext-real Element of REAL
(dist (c1,c2)) - ((dist (w1,x9)) + ((dist (x9,w2)) + (dist (w2,c2)))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (l + 1))) + ((dist (w1,x9)) + ((dist (x9,w2)) + (dist (w2,c2)))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (l + 1))) + ((dist (x9,w2)) + (dist (w2,c2))) is V34() V35() ext-real Element of REAL
(dist (w1,x9)) + ((1 / (2 |^ (l + 1))) + ((dist (x9,w2)) + (dist (w2,c2)))) is V34() V35() ext-real Element of REAL
(dist (c1,c2)) - ((1 / (2 |^ (l + 1))) + ((dist (x9,w2)) + (dist (w2,c2)))) is V34() V35() ext-real Element of REAL
dist (x9,w1) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (l + 1))) + ((dist (x9,w2)) + (dist (w2,c2)))) is V34() V35() ext-real Element of REAL
(dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))) is V34() V35() ext-real Element of REAL
(dist (x9,w2)) + ((dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) is V34() V35() ext-real Element of REAL
(dist (c1,c2)) - ((dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + ((dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1)))) is V34() V35() ext-real Element of REAL
(dist (w2,c2)) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) is V34() V35() ext-real Element of REAL
(dist (c1,c2)) - ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) is V34() V35() ext-real Element of REAL
dist (c2,w2) is V34() V35() ext-real Element of REAL
(1 / (2 |^ (l + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + ((1 / (2 |^ (((m + 1) + k) + 1))) + (1 / (2 |^ (l + 1))))) is V34() V35() ext-real Element of REAL
[M1,M2] is set
{M1,M2} is finite set
{{M1,M2},{M1}} is finite V59() set
[M2,M1] is set
{M2,M1} is finite set
{{M2,M1},{M2}} is finite V59() set
[M1,M2] is set
{M1,M2} is finite set
{{M1,M2},{M1}} is finite V59() set
[M2,M1] is set
{M2,M1} is finite set
{{M2,M1},{M2}} is finite V59() set
{0} is V46() V47() V48() V49() V50() V51() finite set
Seg (((m + 1) + k) + 1) is non empty V46() V47() V48() V49() V50() V51() finite V62(((m + 1) + k) + 1) Element of bool NAT
{0} \/ (Seg (((m + 1) + k) + 1)) is V46() V47() V48() V49() V50() V51() finite set
x is set
w2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
x1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
x1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
w2 is V27() V28() V29() V33() ext-real non negative set
w2 + 1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
w2 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
x1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
x1 is V27() V28() V29() V33() V34() V35() ext-real non negative V46() V47() V48() V49() V50() V51() V53() Element of NAT
PT is non empty TopSpace-like TopStruct
the carrier of PT is non empty set
bool the carrier of PT is non empty set
bool (bool the carrier of PT) is non empty set
metr is Element of bool (bool the carrier of PT)