REAL is V36() V37() V38() V42() set
NAT is V36() V37() V38() V39() V40() V41() V42() Element of bool REAL
bool REAL is non empty set
COMPLEX is V36() V42() set
omega is V36() V37() V38() V39() V40() V41() V42() set
bool omega is non empty set
bool NAT is non empty set
1 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
[:1,1:] is non empty Relation-like set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is Relation-like set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is Relation-like set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
[:2,2:] is non empty Relation-like set
[:[:2,2:],REAL:] is Relation-like set
bool [:[:2,2:],REAL:] is non empty set
{} is empty Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered set
3 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
union {} is finite set
0 is empty Relation-like non-empty empty-yielding functional ordinal natural V27() real ext-real non positive non negative V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered Element of NAT
D is MetrStruct
the carrier of D is set
f is Element of the carrier of D
f is V27() real ext-real set
c4 is V27() real ext-real set
Ball (f,f) is Element of bool the carrier of D
bool the carrier of D is non empty set
Ball (f,c4) is Element of bool the carrier of D
b is Element of the carrier of D
dist (f,b) is V27() real ext-real Element of REAL
D is TopSpace-like TopStruct
the carrier of D is set
bool the carrier of D is non empty set
f is Element of bool the carrier of D
Cl f is closed Element of bool the carrier of D
the Element of f is Element of f
c4 is set
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
[#] D is non empty non proper open closed Element of bool the carrier of D
f is Element of the carrier of D
c4 is set
b is Element of bool the carrier of D
D is set
1TopSp D is strict TopSpace-like TopStruct
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
[#] (bool D) is non empty non proper Element of bool (bool D)
bool (bool D) is non empty set
TopStruct(# D,([#] (bool D)) #) is strict TopStruct
the topology of (1TopSp D) is non empty open Element of bool (bool the carrier of (1TopSp D))
the carrier of (1TopSp D) is set
bool the carrier of (1TopSp D) is non empty set
bool (bool the carrier of (1TopSp D)) is non empty set
D is set
1TopSp D is strict TopSpace-like TopStruct
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
[#] (bool D) is non empty non proper Element of bool (bool D)
bool (bool D) is non empty set
TopStruct(# D,([#] (bool D)) #) is strict TopStruct
the carrier of (1TopSp D) is set
D is set
{D} is non empty finite set
1TopSp {D} is non empty finite strict TopSpace-like T_0 T_1 Hausdorff compact TopStruct
bool {D} is non empty finite V47() Element of bool (bool {D})
bool {D} is non empty finite V47() set
bool (bool {D}) is non empty finite V47() set
[#] (bool {D}) is non empty non proper finite V47() Element of bool (bool {D})
bool (bool {D}) is non empty finite V47() set
TopStruct(# {D},([#] (bool {D})) #) is non empty strict TopStruct
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
f is Element of the carrier of D
{f} is non empty finite compact Element of bool the carrier of D
bool the carrier of D is non empty set
D is TopStruct
the carrier of D is set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
f is Element of bool the carrier of D
{ b1 where b1 is Element of bool the carrier of D : ( b1 in f & not b1 misses f ) } is set
c4 is set
b is Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
f is Element of bool (bool the carrier of D)
c4 is Element of the carrier of D
b is Element of bool the carrier of D
{ b1 where b1 is Element of bool the carrier of D : ( b1 in f & not b1 misses b ) } is set
c is Element of bool the carrier of D
{ b1 where b1 is Element of bool the carrier of D : ( b1 in f & not b1 misses c ) } is set
c is set
V is Element of bool the carrier of D
W is Element of bool the carrier of D
V is Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
f is Element of the carrier of D
[#] D is non empty non proper open closed Element of bool the carrier of D
{ b1 where b1 is Element of bool the carrier of D : ( b1 in f & not b1 misses [#] D ) } is set
D is TopStruct
the carrier of D is set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
f is Element of bool (bool the carrier of D)
c4 is Element of bool (bool the carrier of D)
b is set
c is Element of bool the carrier of D
c is Element of bool the carrier of D
Cl c is Element of bool the carrier of D
b is set
c is Element of bool the carrier of D
c is Element of bool the carrier of D
Cl c is Element of bool the carrier of D
D is TopSpace-like TopStruct
the carrier of D is set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
(D,f) is Element of bool (bool the carrier of D)
f is Element of bool the carrier of D
c4 is Element of bool the carrier of D
Cl c4 is closed Element of bool the carrier of D
D is TopSpace-like TopStruct
the carrier of D is set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
(D,f) is Element of bool (bool the carrier of D)
f is set
the Element of f is Element of f
b is set
c is Element of bool the carrier of D
c is Element of bool the carrier of D
Cl c is closed Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool the carrier of D
{f} is non empty finite Element of bool (bool the carrier of D)
Cl f is closed Element of bool the carrier of D
{(Cl f)} is non empty finite Element of bool (bool the carrier of D)
f is Element of bool (bool the carrier of D)
(D,f) is Element of bool (bool the carrier of D)
c4 is set
b is set
c is Element of bool the carrier of D
Cl c is closed Element of bool the carrier of D
c is Element of bool the carrier of D
c is Element of bool the carrier of D
Cl c is closed Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
(D,f) is Element of bool (bool the carrier of D)
f is Element of bool (bool the carrier of D)
(D,f) is Element of bool (bool the carrier of D)
c4 is set
b is set
c is set
c is Element of bool the carrier of D
V is Element of bool the carrier of D
Cl V is closed Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
(D,f) is Element of bool (bool the carrier of D)
f is Element of bool (bool the carrier of D)
f \/ f is Element of bool (bool the carrier of D)
(D,(f \/ f)) is Element of bool (bool the carrier of D)
(D,f) is Element of bool (bool the carrier of D)
(D,f) \/ (D,f) is Element of bool (bool the carrier of D)
c4 is set
b is Element of bool the carrier of D
c is Element of bool the carrier of D
Cl c is closed Element of bool the carrier of D
c is Element of bool the carrier of D
Cl c is closed Element of bool the carrier of D
b is Element of bool the carrier of D
c is Element of bool the carrier of D
Cl c is closed Element of bool the carrier of D
c is Element of bool the carrier of D
Cl c is closed Element of bool the carrier of D
b is Element of bool the carrier of D
c is Element of bool the carrier of D
Cl c is closed Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
Cl (union f) is closed Element of bool the carrier of D
(D,f) is Element of bool (bool the carrier of D)
union (D,f) is Element of bool the carrier of D
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng f is finite set
dom f is V36() V37() V38() V39() V40() V41() finite Element of bool NAT
c4 is ordinal natural V27() real ext-real non negative set
Seg c4 is V36() V37() V38() V39() V40() V41() finite V50(c4) Element of bool NAT
b is ordinal natural V27() real ext-real non negative set
Seg b is V36() V37() V38() V39() V40() V41() finite V50(b) Element of bool NAT
f .: (Seg b) is finite set
b + 1 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
Seg (b + 1) is non empty V36() V37() V38() V39() V40() V41() finite V50(b + 1) Element of bool NAT
f .: (Seg (b + 1)) is finite set
c is Element of bool (bool the carrier of D)
union c is Element of bool the carrier of D
Cl (union c) is closed Element of bool the carrier of D
(D,c) is Element of bool (bool the carrier of D)
union (D,c) is Element of bool the carrier of D
Im (f,(b + 1)) is set
{(b + 1)} is non empty V36() V37() V38() V39() V40() V41() finite set
f .: {(b + 1)} is finite set
c4 + 1 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
0 + 1 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
c is Element of bool (bool the carrier of D)
f . (b + 1) is set
{(f . (b + 1))} is non empty finite set
union c is Element of bool the carrier of D
(D,c) is Element of bool (bool the carrier of D)
union (D,c) is Element of bool the carrier of D
W is Element of bool the carrier of D
Cl W is closed Element of bool the carrier of D
{(Cl W)} is non empty finite Element of bool (bool the carrier of D)
union {(Cl W)} is Element of bool the carrier of D
Cl (union c) is closed Element of bool the carrier of D
(Seg b) \/ {(b + 1)} is non empty V36() V37() V38() V39() V40() V41() finite set
f .: ((Seg b) \/ {(b + 1)}) is finite set
(f .: (Seg b)) \/ (f .: {(b + 1)}) is finite set
V is Element of bool (bool the carrier of D)
union V is Element of bool the carrier of D
(union V) \/ (union c) is Element of bool the carrier of D
Cl ((union V) \/ (union c)) is closed Element of bool the carrier of D
Cl (union V) is closed Element of bool the carrier of D
(Cl (union V)) \/ (Cl (union c)) is closed Element of bool the carrier of D
(D,V) is Element of bool (bool the carrier of D)
union (D,V) is Element of bool the carrier of D
(union (D,V)) \/ (union (D,c)) is Element of bool the carrier of D
(D,V) \/ (D,c) is Element of bool (bool the carrier of D)
union ((D,V) \/ (D,c)) is Element of bool the carrier of D
Seg 0 is empty Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() V50( 0 ) FinSequence-like FinSequence-membered Element of bool NAT
f .: (Seg 0) is empty Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered set
b is Element of bool (bool the carrier of D)
union b is Element of bool the carrier of D
Cl (union b) is closed Element of bool the carrier of D
(D,b) is Element of bool (bool the carrier of D)
union (D,b) is Element of bool the carrier of D
{} D is empty proper Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered open closed compact Element of bool the carrier of D
f .: (Seg c4) is finite set
f .: {} is empty Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered set
{} D is empty proper Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered open closed compact Element of bool the carrier of D
0 + 1 is non empty ordinal natural V27() real ext-real positive non negative V36() V37() V38() V39() V40() V41() Element of NAT
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
(D,f) is Element of bool (bool the carrier of D)
c4 is set
b is Element of bool the carrier of D
Cl b is closed Element of bool the carrier of D
c is set
F1() is TopSpace-like TopStruct
the carrier of F1() is set
bool the carrier of F1() is non empty set
bool (bool the carrier of F1()) is non empty set
F2() is Element of bool (bool the carrier of F1())
F3() is Element of bool (bool the carrier of F1())
[:F2(),F3():] is Relation-like set
bool [:F2(),F3():] is non empty set
D is set
F4(D) is Element of bool the carrier of F1()
D is Relation-like F2() -defined F3() -valued Function-like V33(F2(),F3()) Element of bool [:F2(),F3():]
f is Element of bool the carrier of F1()
D . f is set
F4(f) is Element of bool the carrier of F1()
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
(D,f) is Element of bool (bool the carrier of D)
c4 is Element of the carrier of D
b is Element of bool the carrier of D
{ b1 where b1 is Element of bool the carrier of D : ( b1 in f & not b1 misses b ) } is set
{ b1 where b1 is Element of bool the carrier of D : ( b1 in (D,f) & not b1 misses b ) } is set
V is Element of bool the carrier of D
Cl V is closed Element of bool the carrier of D
[:f,(D,f):] is Relation-like set
bool [:f,(D,f):] is non empty set
V is Relation-like f -defined (D,f) -valued Function-like V33(f,(D,f)) Element of bool [:f,(D,f):]
dom V is set
V .: { b1 where b1 is Element of bool the carrier of D : ( b1 in f & not b1 misses b ) } is set
W is set
W is Element of bool the carrier of D
V is Element of bool the carrier of D
Cl V is closed Element of bool the carrier of D
V . V is set
W /\ b is Element of bool the carrier of D
c12 is Element of bool the carrier of D
Cl c12 is closed Element of bool the carrier of D
b /\ (Cl c12) is Element of bool the carrier of D
Cl (b /\ (Cl c12)) is closed Element of bool the carrier of D
b /\ c12 is Element of bool the carrier of D
Cl (b /\ c12) is closed Element of bool the carrier of D
c12 /\ b is Element of bool the carrier of D
c12 is Element of bool the carrier of D
W is set
V . W is set
W is set
V . W is set
V is Element of bool the carrier of D
V . V is set
Cl V is closed Element of bool the carrier of D
c12 is Element of bool the carrier of D
z is Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
(D,f) is Element of bool (bool the carrier of D)
union (D,f) is Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
Cl (union f) is closed Element of bool the carrier of D
(D,f) is Element of bool (bool the carrier of D)
union (D,f) is Element of bool the carrier of D
b is Element of the carrier of D
c is Element of bool the carrier of D
{ b1 where b1 is Element of bool the carrier of D : ( b1 in f & not b1 misses c ) } is set
V is Element of bool (bool the carrier of D)
union V is Element of bool the carrier of D
Cl (union V) is closed Element of bool the carrier of D
(D,V) is Element of bool (bool the carrier of D)
union (D,V) is Element of bool the carrier of D
f \ V is Element of bool (bool the carrier of D)
union (f \ V) is Element of bool the carrier of D
Cl (union (f \ V)) is closed Element of bool the carrier of D
W is set
V is set
c12 is Element of bool the carrier of D
union W is set
V \/ (f \ V) is Element of bool (bool the carrier of D)
V \/ f is Element of bool (bool the carrier of D)
(union V) \/ (union (f \ V)) is Element of bool the carrier of D
Cl ((union V) \/ (union (f \ V))) is closed Element of bool the carrier of D
(Cl (union V)) \/ (Cl (union (f \ V))) is closed Element of bool the carrier of D
b is Element of the carrier of D
c is set
c is Element of bool the carrier of D
V is Element of bool the carrier of D
Cl V is closed Element of bool the carrier of D
W is Element of bool the carrier of D
(union f) /\ W is Element of bool the carrier of D
V /\ W is Element of bool the carrier of D
W is set
W is Element of the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
(D,f) is Element of bool (bool the carrier of D)
union (D,f) is Element of bool the carrier of D
b is Element of the carrier of D
c is set
c is Element of bool the carrier of D
V is Element of bool the carrier of D
Cl V is closed Element of bool the carrier of D
W is Element of bool the carrier of D
Cl (union f) is closed Element of bool the carrier of D
{1} is non empty V36() V37() V38() V39() V40() V41() finite set
1TopSp {1} is non empty finite strict TopSpace-like T_0 T_1 Hausdorff compact TopStruct
bool {1} is non empty finite V47() Element of bool (bool {1})
bool {1} is non empty finite V47() set
bool (bool {1}) is non empty finite V47() set
[#] (bool {1}) is non empty non proper finite V47() Element of bool (bool {1})
bool (bool {1}) is non empty finite V47() set
TopStruct(# {1},([#] (bool {1})) #) is non empty strict TopStruct
D is non empty finite strict TopSpace-like T_0 T_1 Hausdorff compact TopStruct
the carrier of D is non empty finite set
bool the carrier of D is non empty finite V47() set
bool (bool the carrier of D) is non empty finite V47() set
f is finite V47() Element of bool (bool the carrier of D)
f is finite V47() Element of bool (bool the carrier of D)
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
f is Element of bool (bool the carrier of D)
c4 is Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
f is Element of bool the carrier of D
f is Element of bool the carrier of D
f ` is Element of bool the carrier of D
the carrier of D \ f is set
bool (bool the carrier of D) is non empty set
c4 is Element of bool (bool the carrier of D)
b is Element of the carrier of D
[#] D is non empty non proper open closed Element of bool the carrier of D
f \/ (f `) is Element of bool the carrier of D
c is Element of bool the carrier of D
c is Element of bool the carrier of D
V is Element of bool the carrier of D
union c4 is Element of bool the carrier of D
c is Element of bool the carrier of D
c is Element of bool the carrier of D
union c4 is Element of bool the carrier of D
c is Element of bool the carrier of D
union c4 is Element of bool the carrier of D
union c4 is Element of bool the carrier of D
b is Element of bool the carrier of D
V is Element of the carrier of D
c is Element of bool the carrier of D
c is Element of bool the carrier of D
b is Element of bool (bool the carrier of D)
{ b1 where b1 is Element of bool the carrier of D : ( b1 in b & not b1 misses f ) } is set
c is Element of bool (bool the carrier of D)
(D,c) is Element of bool (bool the carrier of D)
union (D,c) is Element of bool the carrier of D
(union (D,c)) ` is Element of bool the carrier of D
the carrier of D \ (union (D,c)) is set
V is Element of bool the carrier of D
union c is Element of bool the carrier of D
W is Element of bool the carrier of D
Cl (union c) is closed Element of bool the carrier of D
W is Element of bool the carrier of D
Cl W is closed Element of bool the carrier of D
f /\ (Cl W) is Element of bool the carrier of D
V is Element of bool the carrier of D
V is set
c12 is Element of bool the carrier of D
z is Element of bool the carrier of D
c12 is Element of bool the carrier of D
y is Element of the carrier of D
W is Element of bool the carrier of D
z is Element of bool the carrier of D
y is Element of the carrier of D
W is Element of bool the carrier of D
z is Element of bool the carrier of D
z /\ W is Element of bool the carrier of D
Cl (z /\ W) is closed Element of bool the carrier of D
{} D is empty proper Relation-like non-empty empty-yielding functional V36() V37() V38() V39() V40() V41() V42() finite finite-yielding V47() FinSequence-like FinSequence-membered open closed compact Element of bool the carrier of D
Cl ({} D) is closed Element of bool the carrier of D
z /\ (Cl W) is Element of bool the carrier of D
Cl (z /\ (Cl W)) is closed Element of bool the carrier of D
c12 is Element of bool the carrier of D
W is set
V is Element of the carrier of D
c12 is set
z is Element of bool the carrier of D
f /\ z is Element of bool the carrier of D
W is Element of bool the carrier of D
Cl W is closed Element of bool the carrier of D
W is Element of the carrier of D
V is Element of bool the carrier of D
V is Element of bool the carrier of D
V ` is Element of bool the carrier of D
the carrier of D \ V is set
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
f is Element of the carrier of D
f is Element of bool the carrier of D
f ` is Element of bool the carrier of D
the carrier of D \ f is set
{f} is non empty finite compact Element of bool the carrier of D
b is Element of the carrier of D
c is Element of bool the carrier of D
c is Element of bool the carrier of D
b is Element of bool the carrier of D
c is Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
f is Element of bool the carrier of D
f is Element of bool the carrier of D
c4 is Element of the carrier of D
f ` is Element of bool the carrier of D
the carrier of D \ f is set
b is Element of bool the carrier of D
c is Element of bool the carrier of D
c4 is Element of bool the carrier of D
b is Element of bool the carrier of D
D is MetrStruct
the carrier of D is set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of bool (bool the carrier of D)
f is Element of bool (bool the carrier of D)
c4 is Element of bool the carrier of D
b is Element of the carrier of D
b is Element of the carrier of D
D is MetrStruct
the carrier of D is set
f is Element of the carrier of D
f is V27() real ext-real Element of REAL
Ball (f,f) is Element of bool the carrier of D
bool the carrier of D is non empty set
D is MetrStruct
the carrier of D is set
f is Element of the carrier of D
f is Element of the carrier of D
c4 is V27() real ext-real set
Ball (f,c4) is Element of bool the carrier of D
bool the carrier of D is non empty set
dist (f,f) is V27() real ext-real Element of REAL
b is V27() real ext-real Element of REAL
b - (dist (f,f)) is V27() real ext-real Element of REAL
Ball (f,(b - (dist (f,f)))) is Element of bool the carrier of D
c is Element of the carrier of D
dist (f,c) is V27() real ext-real Element of REAL
(dist (f,f)) + (dist (f,c)) is V27() real ext-real Element of REAL
dist (f,c) is V27() real ext-real Element of REAL
D is MetrStruct
the carrier of D is set
f is V27() real ext-real Element of REAL
f is V27() real ext-real Element of REAL
c4 is Element of the carrier of D
b is Element of the carrier of D
Ball (b,f) is Element of bool the carrier of D
bool the carrier of D is non empty set
c is Element of the carrier of D
Ball (c,f) is Element of bool the carrier of D
(Ball (b,f)) /\ (Ball (c,f)) is Element of bool the carrier of D
c is V27() real ext-real Element of REAL
Ball (c4,c) is Element of bool the carrier of D
V is V27() real ext-real Element of REAL
Ball (c4,V) is Element of bool the carrier of D
min (c,V) is V27() real ext-real Element of REAL
W is V27() real ext-real Element of REAL
Ball (c4,W) is Element of bool the carrier of D
D is MetrStruct
the carrier of D is set
(D) is Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of the carrier of D
f is V27() real ext-real set
Ball (f,f) is Element of bool the carrier of D
c4 is Element of the carrier of D
D is MetrStruct
the carrier of D is set
(D) is Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
f is Element of the carrier of D
D is MetrStruct
the carrier of D is set
bool the carrier of D is non empty set
(D) is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
f is Element of bool the carrier of D
f is Element of bool the carrier of D
f /\ f is Element of bool the carrier of D
c4 is Element of the carrier of D
b is V27() real ext-real Element of REAL
Ball (c4,b) is Element of bool the carrier of D
c is V27() real ext-real Element of REAL
Ball (c4,c) is Element of bool the carrier of D
min (b,c) is V27() real ext-real Element of REAL
c is V27() real ext-real Element of REAL
Ball (c4,c) is Element of bool the carrier of D
D is MetrStruct
the carrier of D is set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
(D) is Element of bool (bool the carrier of D)
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
f is Element of the carrier of D
c4 is set
b is Element of bool the carrier of D
c is V27() real ext-real Element of REAL
Ball (f,c) is Element of bool the carrier of D
D is MetrStruct
the carrier of D is set
(D) is Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D,(D) #) is strict TopStruct
the carrier of TopStruct(# the carrier of D,(D) #) is set
bool the carrier of TopStruct(# the carrier of D,(D) #) is non empty set
the topology of TopStruct(# the carrier of D,(D) #) is open Element of bool (bool the carrier of TopStruct(# the carrier of D,(D) #))
bool (bool the carrier of TopStruct(# the carrier of D,(D) #)) is non empty set
f is Element of bool the carrier of TopStruct(# the carrier of D,(D) #)
c4 is Element of bool the carrier of TopStruct(# the carrier of D,(D) #)
f /\ c4 is Element of bool the carrier of TopStruct(# the carrier of D,(D) #)
f is Element of bool (bool the carrier of TopStruct(# the carrier of D,(D) #))
union f is Element of bool the carrier of TopStruct(# the carrier of D,(D) #)
D is MetrStruct
the carrier of D is set
(D) is Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D,(D) #) is strict TopStruct
D is MetrStruct
(D) is TopStruct
the carrier of D is set
(D) is Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D,(D) #) is strict TopStruct
D is non empty MetrStruct
(D) is strict TopSpace-like TopStruct
the carrier of D is non empty set
(D) is Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D,(D) #) is non empty strict TopStruct
D is non empty Reflexive discerning V96() triangle Discerning MetrStruct
(D) is non empty strict TopSpace-like TopStruct
the carrier of D is non empty set
(D) is Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D,(D) #) is non empty strict TopStruct
the carrier of (D) is non empty set
bool the carrier of (D) is non empty set
f is Element of the carrier of (D)
c4 is Element of the carrier of (D)
b is Element of the carrier of D
c is Element of the carrier of D
dist (b,c) is V27() real ext-real Element of REAL
(dist (b,c)) / 2 is V27() real ext-real Element of REAL
Ball (c,((dist (b,c)) / 2)) is Element of bool the carrier of D
Ball (b,((dist (b,c)) / 2)) is Element of bool the carrier of D
W is Element of bool the carrier of (D)
V is Element of bool the carrier of (D)
W /\ V is Element of bool the carrier of (D)
c12 is set
z is Element of the carrier of D
dist (c,z) is V27() real ext-real Element of REAL
dist (b,z) is V27() real ext-real Element of REAL
((dist (b,c)) / 2) + ((dist (b,c)) / 2) is V27() real ext-real Element of REAL
(dist (b,z)) + (dist (c,z)) is V27() real ext-real Element of REAL
dist (b,b) is V27() real ext-real Element of REAL
dist (c,c) is V27() real ext-real Element of REAL
V is Element of bool the carrier of (D)
W is Element of bool the carrier of (D)
the non empty Reflexive discerning V96() triangle Discerning MetrStruct is non empty Reflexive discerning V96() triangle Discerning MetrStruct
( the non empty Reflexive discerning V96() triangle Discerning MetrStruct ) is non empty strict TopSpace-like TopStruct
the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct is non empty set
( the non empty Reflexive discerning V96() triangle Discerning MetrStruct ) is Element of bool (bool the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct )
bool the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct is non empty set
bool (bool the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct ) is non empty set
TopStruct(# the carrier of the non empty Reflexive discerning V96() triangle Discerning MetrStruct ,( the non empty Reflexive discerning V96() triangle Discerning MetrStruct ) #) is non empty strict TopStruct
D is set
[:D,D:] is Relation-like set
[:[:D,D:],REAL:] is Relation-like set
bool [:[:D,D:],REAL:] is non empty set
D is set
[:D,D:] is Relation-like set
[:[:D,D:],REAL:] is Relation-like set
bool [:[:D,D:],REAL:] is non empty set
f is Relation-like [:D,D:] -defined REAL -valued Function-like V33([:D,D:], REAL ) Element of bool [:[:D,D:],REAL:]
MetrStruct(# D,f #) is strict MetrStruct
c4 is Reflexive discerning V96() triangle MetrStruct
the carrier of c4 is set
the distance of c4 is Relation-like [: the carrier of c4, the carrier of c4:] -defined REAL -valued Function-like V33([: the carrier of c4, the carrier of c4:], REAL ) Element of bool [:[: the carrier of c4, the carrier of c4:],REAL:]
[: the carrier of c4, the carrier of c4:] is Relation-like set
[:[: the carrier of c4, the carrier of c4:],REAL:] is Relation-like set
bool [:[: the carrier of c4, the carrier of c4:],REAL:] is non empty set
b is Element of the carrier of c4
c is Element of the carrier of c4
the distance of c4 . (b,c) is V27() real ext-real Element of REAL
the distance of c4 . (c,b) is V27() real ext-real Element of REAL
c is Element of the carrier of c4
the distance of c4 . (b,c) is V27() real ext-real Element of REAL
the distance of c4 . (c,c) is V27() real ext-real Element of REAL
( the distance of c4 . (b,c)) + ( the distance of c4 . (c,c)) is V27() real ext-real Element of REAL
dist (b,c) is V27() real ext-real Element of REAL
dist (c,b) is V27() real ext-real Element of REAL
dist (b,c) is V27() real ext-real Element of REAL
dist (c,c) is V27() real ext-real Element of REAL
the carrier of MetrStruct(# D,f #) is set
c4 is Element of the carrier of MetrStruct(# D,f #)
b is Element of the carrier of MetrStruct(# D,f #)
dist (c4,b) is V27() real ext-real Element of REAL
dist (b,c4) is V27() real ext-real Element of REAL
c is Element of the carrier of MetrStruct(# D,f #)
dist (c4,c) is V27() real ext-real Element of REAL
dist (b,c) is V27() real ext-real Element of REAL
(dist (c4,b)) + (dist (b,c)) is V27() real ext-real Element of REAL
the distance of MetrStruct(# D,f #) is Relation-like [: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):] -defined REAL -valued Function-like V33([: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):],REAL:]
[: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):] is Relation-like set
[:[: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):],REAL:] is Relation-like set
bool [:[: the carrier of MetrStruct(# D,f #), the carrier of MetrStruct(# D,f #):],REAL:] is non empty set
the distance of MetrStruct(# D,f #) . (c4,b) is V27() real ext-real Element of REAL
the distance of MetrStruct(# D,f #) . (b,c4) is V27() real ext-real Element of REAL
the distance of MetrStruct(# D,f #) . (c4,c) is V27() real ext-real Element of REAL
the distance of MetrStruct(# D,f #) . (b,c) is V27() real ext-real Element of REAL
D is set
[:D,D:] is Relation-like set
[:[:D,D:],REAL:] is Relation-like set
bool [:[:D,D:],REAL:] is non empty set
f is Relation-like [:D,D:] -defined REAL -valued Function-like V33([:D,D:], REAL ) Element of bool [:[:D,D:],REAL:]
MetrStruct(# D,f #) is strict MetrStruct
the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct is non empty strict Reflexive discerning V96() triangle Discerning MetrStruct
( the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ) is non empty strict TopSpace-like TopStruct
the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct is non empty set
( the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ) is Element of bool (bool the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct )
bool the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct is non empty set
bool (bool the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ) is non empty set
TopStruct(# the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ,( the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct ) #) is non empty strict TopStruct
f is non empty strict TopSpace-like TopStruct
the carrier of f is non empty set
[: the carrier of f, the carrier of f:] is non empty Relation-like set
[:[: the carrier of f, the carrier of f:],REAL:] is Relation-like set
bool [:[: the carrier of f, the carrier of f:],REAL:] is non empty set
the distance of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct is Relation-like [: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :] -defined REAL -valued Function-like V33([: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :], REAL ) Element of bool [:[: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :],REAL:]
[: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :] is non empty Relation-like set
[:[: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :],REAL:] is Relation-like set
bool [:[: the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct , the carrier of the non empty strict Reflexive discerning V96() triangle Discerning MetrStruct :],REAL:] is non empty set
f is Relation-like [: the carrier of f, the carrier of f:] -defined REAL -valued Function-like V33([: the carrier of f, the carrier of f:], REAL ) Element of bool [:[: the carrier of f, the carrier of f:],REAL:]
( the carrier of f,f) is strict Reflexive discerning V96() triangle MetrStruct
(( the carrier of f,f)) is Element of bool (bool the carrier of ( the carrier of f,f))
the carrier of ( the carrier of f,f) is set
bool the carrier of ( the carrier of f,f) is non empty set
bool (bool the carrier of ( the carrier of f,f)) is non empty set
the topology of f is non empty open Element of bool (bool the carrier of f)
bool the carrier of f is non empty set
bool (bool the carrier of f) is non empty set
D is non empty set
[:D,D:] is non empty Relation-like set
[:[:D,D:],REAL:] is Relation-like set
bool [:[:D,D:],REAL:] is non empty set
f is Relation-like [:D,D:] -defined REAL -valued Function-like V33([:D,D:], REAL ) Element of bool [:[:D,D:],REAL:]
(D,f) is strict Reflexive discerning V96() triangle MetrStruct
MetrStruct(# D,f #) is strict MetrStruct