REAL is non empty non trivial non finite V169() V170() V171() V175() V269() V270() V272() set
NAT is ordinal non trivial non finite cardinal limit_cardinal V169() V170() V171() V172() V173() V174() V175() V269() Element of bool REAL
bool REAL is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V169() V175() set
omega is ordinal non trivial non finite cardinal limit_cardinal V169() V170() V171() V172() V173() V174() V175() V269() set
bool omega is non empty non trivial non finite set
[:NAT,REAL:] is Relation-like non trivial non finite V159() V160() V161() set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
RAT is non empty non trivial non finite V169() V170() V171() V172() V175() set
INT is non empty non trivial non finite V169() V170() V171() V172() V173() V175() set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V159() V160() V161() set
bool [:REAL,REAL:] is non empty non trivial non finite set
K408() is non empty V118() L9()
the carrier of K408() is non empty set
K413() is non empty V118() V140() V141() V142() V144() V191() V192() V193() V194() V195() V196() L9()
K414() is non empty V118() V142() V144() V194() V195() V196() M18(K413())
K415() is non empty V118() V140() V142() V144() V194() V195() V196() V197() M21(K413(),K414())
K417() is non empty V118() V140() V142() V144() L9()
K418() is non empty V118() V140() V142() V144() V197() M18(K417())
1 is ordinal natural non empty V28() real ext-real positive non negative finite cardinal V99() rational V169() V170() V171() V172() V173() V174() V267() V268() V269() V270() V271() Element of NAT
[:1,1:] is Relation-like RAT -valued INT -valued non empty finite V159() V160() V161() V162() set
bool [:1,1:] is non empty finite V37() set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued non empty finite V159() V160() V161() V162() set
bool [:[:1,1:],1:] is non empty finite V37() set
[:[:1,1:],REAL:] is Relation-like non empty non trivial non finite V159() V160() V161() set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V159() V160() V161() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
2 is ordinal natural non empty V28() real ext-real positive non negative finite cardinal V99() rational V169() V170() V171() V172() V173() V174() V267() V268() V269() V270() V271() Element of NAT
[:2,2:] is Relation-like RAT -valued INT -valued non empty finite V159() V160() V161() V162() set
[:[:2,2:],REAL:] is Relation-like non empty non trivial non finite V159() V160() V161() set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
K525() is non empty strict TopSpace-like V229() TopStruct
the carrier of K525() is non empty V169() V170() V171() set
K454() is V201() V229() L14()
R^1 is non empty strict TopSpace-like V229() TopStruct
I[01] is non empty strict TopSpace-like V229() SubSpace of R^1
TOP-REAL 2 is non empty TopSpace-like V116() V181() V182() V241() V242() V243() V244() V245() V246() V247() V253() L16()
the carrier of (TOP-REAL 2) is non empty set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V159() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V159() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V159() V160() V161() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V159() V160() V161() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V159() V160() V161() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V159() V160() V161() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued V159() V160() V161() V162() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued V159() V160() V161() V162() set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty V28() real ext-real non positive non negative finite finite-yielding V37() cardinal {} -element Function-yielding V65() FinSequence-like FinSubsequence-like FinSequence-membered V159() V160() V161() V162() V169() V170() V171() V172() V173() V174() V175() V269() V270() V271() V272() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty V28() real ext-real non positive non negative finite finite-yielding V37() cardinal {} -element Function-yielding V65() FinSequence-like FinSubsequence-like FinSequence-membered V159() V160() V161() V162() V169() V170() V171() V172() V173() V174() V175() V269() V270() V271() V272() set
3 is ordinal natural non empty V28() real ext-real positive non negative finite cardinal V99() rational V169() V170() V171() V172() V173() V174() V267() V268() V269() V270() V271() Element of NAT
0 is ordinal natural V28() real ext-real finite cardinal V99() rational V169() V170() V171() V172() V173() V174() V269() V270() V271() Element of NAT
Sorgenfrey-line is non empty strict TopSpace-like TopStruct
{ [.b1,b2.[ where b1, b2 is V28() real ext-real Element of REAL : ( not b2 <= b1 & b2 is rational ) } is set
the carrier of Sorgenfrey-line is non empty set
bool the carrier of Sorgenfrey-line is non empty set
len RAT is ordinal non empty non trivial non finite cardinal set
continuum is ordinal non trivial non finite cardinal set
len REAL is ordinal non empty non trivial non finite cardinal set
exp (2,omega) is ordinal cardinal set
Seg 1 is non empty trivial finite 1 -element V169() V170() V171() V172() V173() V174() V267() V268() V269() V270() V271() Element of bool NAT
{1} is non empty trivial finite V37() 1 -element V169() V170() V171() V172() V173() V174() V267() V268() V269() V270() V271() set
Seg 2 is non empty finite 2 -element V169() V170() V171() V172() V173() V174() V267() V268() V269() V270() V271() Element of bool NAT
{1,2} is finite V37() V169() V170() V171() V172() V173() V174() V269() V270() V271() set
omega *` omega is ordinal cardinal set
[.0,1.] is V169() V170() V171() V272() Element of bool REAL
bool the carrier of K525() is non empty set
- 1 is non empty V28() real ext-real non positive negative rational Element of REAL
Closed-Interval-TSpace ((- 1),1) is non empty strict TopSpace-like V229() SubSpace of R^1
the carrier of (Closed-Interval-TSpace ((- 1),1)) is non empty V169() V170() V171() set
the carrier of I[01] is non empty V169() V170() V171() set
[: the carrier of I[01], the carrier of (Closed-Interval-TSpace ((- 1),1)):] is Relation-like non empty V159() V160() V161() set
bool [: the carrier of I[01], the carrier of (Closed-Interval-TSpace ((- 1),1)):] is non empty set
the carrier of R^1 is non empty V169() V170() V171() set
proj1 {} is set
proj2 {} is set
bool the carrier of R^1 is non empty set
-infty is non empty non real ext-real non positive negative set
+infty is non empty non real ext-real positive non negative set
K200(-infty,+infty) is V267() V268() V272() set
X is Relation-like Function-like set
B is Relation-like Function-like set
X +* B is Relation-like Function-like set
uB is set
(X +* B) " uB is set
X " uB is set
B " uB is set
(X " uB) \/ (B " uB) is set
x is set
proj1 (X +* B) is set
proj1 X is set
proj1 B is set
(proj1 X) \/ (proj1 B) is set
(X +* B) . x is set
X . x is set
B . x is set
X is Relation-like Function-like set
proj1 X is set
B is Relation-like Function-like set
proj1 B is set
X +* B is Relation-like Function-like set
uB is set
(X +* B) " uB is set
X " uB is set
B " uB is set
(X " uB) \/ (B " uB) is set
B is set
X is set
uB is Relation-like Function-like set
proj1 uB is set
X .--> uB is Relation-like {X} -defined Function-like one-to-one finite Function-yielding V65() set
{X} is non empty trivial finite 1 -element set
{X} --> uB is Relation-like {X} -defined {uB} -valued Function-like constant non empty total quasi_total finite Function-yielding V65() Element of bool [:{X},{uB}:]
{uB} is functional non empty trivial finite 1 -element set
[:{X},{uB}:] is Relation-like non empty finite set
bool [:{X},{uB}:] is non empty finite V37() set
commute (X .--> uB) is Relation-like Function-like Function-yielding V65() set
uncurry (X .--> uB) is Relation-like Function-like set
curry' (uncurry (X .--> uB)) is Relation-like Function-like set
(commute (X .--> uB)) . B is Relation-like Function-like set
uB . B is set
X .--> (uB . B) is Relation-like {X} -defined Function-like one-to-one finite set
{X} --> (uB . B) is Relation-like {X} -defined {(uB . B)} -valued Function-like constant non empty total quasi_total finite Element of bool [:{X},{(uB . B)}:]
{(uB . B)} is non empty trivial finite 1 -element set
[:{X},{(uB . B)}:] is Relation-like non empty finite set
bool [:{X},{(uB . B)}:] is non empty finite V37() set
dom (X .--> uB) is trivial finite Element of bool {X}
bool {X} is non empty finite V37() set
proj2 uB is set
Funcs ((proj1 uB),(proj2 uB)) is functional set
proj2 (X .--> uB) is finite set
Funcs ({X},(Funcs ((proj1 uB),(proj2 uB)))) is functional set
(X .--> uB) . X is Relation-like Function-like set
((commute (X .--> uB)) . B) . X is set
proj1 ((commute (X .--> uB)) . B) is set
X is set
B is Relation-like Function-like set
commute B is Relation-like Function-like Function-yielding V65() set
uncurry B is Relation-like Function-like set
curry' (uncurry B) is Relation-like Function-like set
proj1 (commute B) is set
proj1 B is set
proj1 (uncurry B) is set
proj2 (proj1 (uncurry B)) is set
uB is set
[uB,X] is V22() set
{uB,X} is finite set
{uB} is non empty trivial finite 1 -element set
{{uB,X},{uB}} is finite V37() set
x is set
V9 is set
[x,V9] is V22() set
{x,V9} is finite set
{x} is non empty trivial finite 1 -element set
{{x,V9},{x}} is finite V37() set
V is Relation-like Function-like set
B . x is set
proj1 V is set
x9 is set
r is Relation-like Function-like set
B . x9 is set
proj1 r is set
uB is set
x is Relation-like Function-like set
B . uB is set
proj1 x is set
[uB,X] is V22() set
{uB,X} is finite set
{uB} is non empty trivial finite 1 -element set
{{uB,X},{uB}} is finite V37() set
X is set
B is set
uB is Relation-like Function-like set
commute uB is Relation-like Function-like Function-yielding V65() set
uncurry uB is Relation-like Function-like set
curry' (uncurry uB) is Relation-like Function-like set
(commute uB) . B is Relation-like Function-like set
proj1 ((commute uB) . B) is set
proj1 uB is set
uB . X is set
proj1 (uncurry uB) is set
proj2 uB is set
union (proj2 uB) is set
proj1 (union (proj2 uB)) is set
[:(proj1 uB),(proj1 (union (proj2 uB))):] is Relation-like set
x is set
V is set
x9 is set
[V,x9] is V22() set
{V,x9} is finite set
{V} is non empty trivial finite 1 -element set
{{V,x9},{V}} is finite V37() set
V9 is Relation-like Function-like set
uB . V is set
proj1 V9 is set
uncurry' (commute uB) is Relation-like Function-like set
proj1 (commute uB) is set
[X,B] is V22() set
{X,B} is finite set
{X} is non empty trivial finite 1 -element set
{{X,B},{X}} is finite V37() set
x is set
V9 is set
[x,V9] is V22() set
{x,V9} is finite set
{x} is non empty trivial finite 1 -element set
{{x,V9},{x}} is finite V37() set
V is Relation-like Function-like set
uB . x is set
proj1 V is set
x9 is Relation-like Function-like set
proj1 x9 is set
x is Relation-like Function-like set
proj1 x is set
X is set
B is set
uB is Relation-like Function-like set
proj1 uB is set
x is Relation-like Function-like set
uB . X is set
proj1 x is set
commute uB is Relation-like Function-like Function-yielding V65() set
uncurry uB is Relation-like Function-like set
curry' (uncurry uB) is Relation-like Function-like set
(commute uB) . B is Relation-like Function-like set
((commute uB) . B) . X is set
x . B is set
[X,B] is V22() set
{X,B} is finite set
{X} is non empty trivial finite 1 -element set
{{X,B},{X}} is finite V37() set
proj1 (uncurry uB) is set
[X,B] `2 is set
[X,B] `1 is set
(uncurry uB) . (X,B) is set
(uncurry uB) . [X,B] is set
X is set
x is Relation-like Function-like set
B is Relation-like Function-like set
uB is Relation-like Function-like set
B \/ uB is Relation-like set
commute x is Relation-like Function-like Function-yielding V65() set
uncurry x is Relation-like Function-like set
curry' (uncurry x) is Relation-like Function-like set
(commute x) . X is Relation-like Function-like set
commute B is Relation-like Function-like Function-yielding V65() set
uncurry B is Relation-like Function-like set
curry' (uncurry B) is Relation-like Function-like set
(commute B) . X is Relation-like Function-like set
commute uB is Relation-like Function-like Function-yielding V65() set
uncurry uB is Relation-like Function-like set
curry' (uncurry uB) is Relation-like Function-like set
(commute uB) . X is Relation-like Function-like set
((commute B) . X) \/ ((commute uB) . X) is Relation-like set
V is set
V9 is set
[V,V9] is V22() set
{V,V9} is finite set
{V} is non empty trivial finite 1 -element set
{{V,V9},{V}} is finite V37() set
((commute x) . X) . V is set
proj1 ((commute x) . X) is set
proj1 x is set
x . V is set
x9 is Relation-like Function-like set
proj1 x9 is set
[V,x9] is V22() set
{V,x9} is finite set
{{V,x9},{V}} is finite V37() set
proj1 B is set
B . V is set
proj1 uB is set
uB . V is set
proj1 ((commute B) . X) is set
((commute B) . X) . V is set
x9 . X is set
proj1 ((commute uB) . X) is set
((commute uB) . X) . V is set
x9 is Relation-like Function-like set
proj1 x9 is set
x9 . X is set
[V,x9] is V22() set
{V,x9} is finite set
{{V,x9},{V}} is finite V37() set
x9 is Relation-like Function-like set
proj1 x9 is set
x9 . X is set
[V,x9] is V22() set
{V,x9} is finite set
{{V,x9},{V}} is finite V37() set
X is set
B is set
<*X,B*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
product <*X,B*> is set
[:X,B:] is Relation-like set
len (product <*X,B*>) is ordinal cardinal set
len X is ordinal cardinal set
len B is ordinal cardinal set
(len X) *` (len B) is ordinal cardinal set
uB is Relation-like Function-like set
proj1 uB is set
<*X,B*> . 2 is set
dom <*X,B*> is non empty finite 2 -element V169() V170() V171() V172() V173() V174() V267() V268() V269() V270() V271() Element of bool NAT
{1,2} is finite V37() V169() V170() V171() V172() V173() V174() V269() V270() V271() Element of bool REAL
<*X,B*> . 1 is set
proj2 uB is set
x is set
V is set
uB . x is set
uB . V is set
V9 is Relation-like Function-like set
proj1 V9 is set
x9 is Relation-like Function-like set
proj1 x9 is set
x9 . 1 is set
x9 . 2 is set
[(x9 . 1),(x9 . 2)] is V22() set
{(x9 . 1),(x9 . 2)} is finite set
{(x9 . 1)} is non empty trivial finite 1 -element set
{{(x9 . 1),(x9 . 2)},{(x9 . 1)}} is finite V37() set
V9 . 1 is set
V9 . 2 is set
[(V9 . 1),(V9 . 2)] is V22() set
{(V9 . 1),(V9 . 2)} is finite set
{(V9 . 1)} is non empty trivial finite 1 -element set
{{(V9 . 1),(V9 . 2)},{(V9 . 1)}} is finite V37() set
r is set
x9 . r is set
V9 . r is set
x is set
V is set
uB . V is set
V9 is Relation-like Function-like set
proj1 V9 is set
V9 . 1 is set
V9 . 2 is set
[(V9 . 1),(V9 . 2)] is V22() set
{(V9 . 1),(V9 . 2)} is finite set
{(V9 . 1)} is non empty trivial finite 1 -element set
{{(V9 . 1),(V9 . 2)},{(V9 . 1)}} is finite V37() set
x is set
x `1 is set
x `2 is set
<*(x `1),(x `2)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*(x `1),(x `2)*> . 1 is set
<*(x `1),(x `2)*> . 2 is set
[(x `1),(x `2)] is V22() set
{(x `1),(x `2)} is finite set
{(x `1)} is non empty trivial finite 1 -element set
{{(x `1),(x `2)},{(x `1)}} is finite V37() set
uB . <*(x `1),(x `2)*> is set
len [:X,B:] is ordinal cardinal set
[:(len X),(len B):] is Relation-like set
len [:(len X),(len B):] is ordinal cardinal set
F3() is non empty set
F1() is non empty set
F2() is non empty set
[:F3(),F2():] is Relation-like non empty set
bool [:F3(),F2():] is non empty set
X is set
F4(X) is set
F5(X) is set
X is Relation-like F3() -defined F2() -valued Function-like non empty total quasi_total Element of bool [:F3(),F2():]
B is Element of F1()
X . B is set
F4(B) is set
F5(B) is set
F3() is non empty set
F1() is non empty set
F2() is non empty set
[:F3(),F2():] is Relation-like non empty set
bool [:F3(),F2():] is non empty set
{ b1 where b1 is Element of F3() : ( P1[b1] or P2[b1] ) } is set
B is Relation-like Function-like set
proj1 B is set
proj2 B is set
uB is set
x is set
B . x is set
F6(x) is set
uB is Relation-like F3() -defined F2() -valued Function-like non empty total quasi_total Element of bool [:F3(),F2():]
x is Element of F1()
uB . x is set
F4(x) is set
F5(x) is set
F6(x) is set
B is non empty set
uB is set
F4(uB) is set
F5(uB) is set
x is Element of F3()
x is Element of F3()
[:B,F2():] is Relation-like non empty set
bool [:B,F2():] is non empty set
uB is Relation-like B -defined F2() -valued Function-like non empty total quasi_total Element of bool [:B,F2():]
x is set
uB . x is set
F6(x) is set
F5(x) is set
F4(x) is set
x is Relation-like F3() -defined F2() -valued Function-like non empty total quasi_total Element of bool [:F3(),F2():]
V is Element of F1()
x . V is set
F4(V) is set
F5(V) is set
F6(V) is set
uB . V is set
X is V28() real ext-real set
B is V28() real ext-real set
|[X,B]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|.|[X,B]|.| is V28() real ext-real non negative Element of REAL
|.|[X,B]|.| ^2 is V28() real ext-real Element of REAL
|.|[X,B]|.| * |.|[X,B]|.| is V28() real ext-real non negative set
X ^2 is V28() real ext-real set
X * X is V28() real ext-real set
B ^2 is V28() real ext-real set
B * B is V28() real ext-real set
(X ^2) + (B ^2) is V28() real ext-real set
|[X,B]| `2 is V28() real ext-real Element of REAL
|[X,B]| `1 is V28() real ext-real Element of REAL
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of X is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
uB is closed Element of bool the carrier of X
X | uB is strict TopSpace-like SubSpace of X
the carrier of (X | uB) is set
[: the carrier of (X | uB), the carrier of B:] is Relation-like set
bool [: the carrier of (X | uB), the carrier of B:] is non empty set
x is closed Element of bool the carrier of X
X | x is strict TopSpace-like SubSpace of X
the carrier of (X | x) is set
[: the carrier of (X | x), the carrier of B:] is Relation-like set
bool [: the carrier of (X | x), the carrier of B:] is non empty set
uB \/ x is closed Element of bool the carrier of X
X | (uB \/ x) is strict TopSpace-like SubSpace of X
the carrier of (X | (uB \/ x)) is set
[: the carrier of (X | (uB \/ x)), the carrier of B:] is Relation-like set
bool [: the carrier of (X | (uB \/ x)), the carrier of B:] is non empty set
V is Relation-like the carrier of (X | uB) -defined the carrier of B -valued Function-like total quasi_total continuous Element of bool [: the carrier of (X | uB), the carrier of B:]
V9 is Relation-like the carrier of (X | x) -defined the carrier of B -valued Function-like total quasi_total continuous Element of bool [: the carrier of (X | x), the carrier of B:]
V +* V9 is Relation-like Function-like set
dom V9 is Element of bool the carrier of (X | x)
bool the carrier of (X | x) is non empty set
dom V is Element of bool the carrier of (X | uB)
bool the carrier of (X | uB) is non empty set
proj2 (V +* V9) is set
rng V is Element of bool the carrier of B
bool the carrier of B is non empty set
rng V9 is Element of bool the carrier of B
(rng V) \/ (rng V9) is Element of bool the carrier of B
proj1 (V +* V9) is set
(dom V) \/ (dom V9) is set
x9 is Relation-like the carrier of (X | (uB \/ x)) -defined the carrier of B -valued Function-like total quasi_total Element of bool [: the carrier of (X | (uB \/ x)), the carrier of B:]
r is Element of bool the carrier of B
x9 " r is Element of bool the carrier of (X | (uB \/ x))
bool the carrier of (X | (uB \/ x)) is non empty set
[#] (X | (uB \/ x)) is non proper open closed dense Element of bool the carrier of (X | (uB \/ x))
V " r is Element of bool the carrier of (X | uB)
[#] (X | uB) is non proper open closed dense Element of bool the carrier of (X | uB)
f is Element of bool the carrier of X
f /\ ([#] (X | uB)) is Element of bool the carrier of (X | uB)
V9 " r is Element of bool the carrier of (X | x)
[#] (X | x) is non proper open closed dense Element of bool the carrier of (X | x)
f is Element of bool the carrier of X
f /\ ([#] (X | x)) is Element of bool the carrier of (X | x)
f /\ uB is Element of bool the carrier of X
f /\ x is Element of bool the carrier of X
(f /\ uB) \/ (f /\ x) is Element of bool the carrier of X
(V " r) \/ (V9 " r) is set
((V " r) \/ (V9 " r)) /\ (uB \/ x) is Element of bool the carrier of X
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of X is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
uB is closed Element of bool the carrier of X
x is closed Element of bool the carrier of X
X | uB is strict TopSpace-like SubSpace of X
the carrier of (X | uB) is set
[: the carrier of (X | uB), the carrier of B:] is Relation-like set
bool [: the carrier of (X | uB), the carrier of B:] is non empty set
X | x is strict TopSpace-like SubSpace of X
the carrier of (X | x) is set
[: the carrier of (X | x), the carrier of B:] is Relation-like set
bool [: the carrier of (X | x), the carrier of B:] is non empty set
uB \/ x is closed Element of bool the carrier of X
X | (uB \/ x) is strict TopSpace-like SubSpace of X
the carrier of (X | (uB \/ x)) is set
[: the carrier of (X | (uB \/ x)), the carrier of B:] is Relation-like set
bool [: the carrier of (X | (uB \/ x)), the carrier of B:] is non empty set
V is Relation-like the carrier of (X | uB) -defined the carrier of B -valued Function-like total quasi_total continuous Element of bool [: the carrier of (X | uB), the carrier of B:]
V9 is Relation-like the carrier of (X | x) -defined the carrier of B -valued Function-like total quasi_total continuous Element of bool [: the carrier of (X | x), the carrier of B:]
V +* V9 is Relation-like Function-like set
dom V9 is Element of bool the carrier of (X | x)
bool the carrier of (X | x) is non empty set
dom V is Element of bool the carrier of (X | uB)
bool the carrier of (X | uB) is non empty set
X is TopSpace-like TopStruct
the carrier of X is set
bool the carrier of X is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
[: the carrier of X, the carrier of B:] is Relation-like set
bool [: the carrier of X, the carrier of B:] is non empty set
uB is open closed Element of bool the carrier of X
X | uB is strict TopSpace-like SubSpace of X
the carrier of (X | uB) is set
[: the carrier of (X | uB), the carrier of B:] is Relation-like set
bool [: the carrier of (X | uB), the carrier of B:] is non empty set
uB ` is open closed Element of bool the carrier of X
the carrier of X \ uB is set
X | (uB `) is strict TopSpace-like SubSpace of X
the carrier of (X | (uB `)) is set
[: the carrier of (X | (uB `)), the carrier of B:] is Relation-like set
bool [: the carrier of (X | (uB `)), the carrier of B:] is non empty set
x is Relation-like the carrier of (X | uB) -defined the carrier of B -valued Function-like total quasi_total continuous Element of bool [: the carrier of (X | uB), the carrier of B:]
V is Relation-like the carrier of (X | (uB `)) -defined the carrier of B -valued Function-like total quasi_total continuous Element of bool [: the carrier of (X | (uB `)), the carrier of B:]
x +* V is Relation-like Function-like set
uB \/ (uB `) is open closed Element of bool the carrier of X
[#] X is non proper open closed dense Element of bool the carrier of X
X | (uB \/ (uB `)) is strict TopSpace-like SubSpace of X
the topology of X is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is strict TopSpace-like TopStruct
the carrier of (X | (uB \/ (uB `))) is set
[: the carrier of (X | (uB \/ (uB `))), the carrier of B:] is Relation-like set
bool [: the carrier of (X | (uB \/ (uB `))), the carrier of B:] is non empty set
the topology of B is non empty Element of bool (bool the carrier of B)
bool the carrier of B is non empty set
bool (bool the carrier of B) is non empty set
TopStruct(# the carrier of B, the topology of B #) is non empty strict TopSpace-like TopStruct
X is ordinal natural V28() real ext-real finite cardinal V99() rational V169() V170() V171() V172() V173() V174() V269() V270() V271() Element of NAT
TOP-REAL X is non empty TopSpace-like V116() V181() V182() V241() V242() V243() V244() V245() V246() V247() V253() L16()
the carrier of (TOP-REAL X) is non empty set
B is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
uB is non empty V28() real ext-real positive non negative set
Ball (B,uB) is Element of bool the carrier of (TOP-REAL X)
bool the carrier of (TOP-REAL X) is non empty set
B - B is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
K391(B,B) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
0. (TOP-REAL X) is Relation-like NAT -defined Function-like finite X -element V74( TOP-REAL X) FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
the ZeroF of (TOP-REAL X) is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
|.(B - B).| is V28() real ext-real non negative Element of REAL
{ |[b1,0]| where b1 is V28() real ext-real Element of REAL : verum } is set
bool the carrier of (TOP-REAL 2) is non empty set
B is set
uB is V28() real ext-real Element of REAL
|[uB,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V28() real ext-real Element of REAL : 0 <= b2 } is set
B is set
uB is V28() real ext-real Element of REAL
x is V28() real ext-real Element of REAL
|[uB,x]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
() is Element of bool the carrier of (TOP-REAL 2)
() is Element of bool the carrier of (TOP-REAL 2)
X is set
B is set
<*X,B*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
uB is V28() real ext-real Element of REAL
|[uB,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
<*X,B*> . 1 is set
uB is V28() real ext-real Element of REAL
|[uB,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
uB is V28() real ext-real Element of REAL
|[uB,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
<*X,B*> . 2 is set
uB is V28() real ext-real Element of REAL
|[uB,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
<*X,0*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
X is V28() real ext-real set
B is V28() real ext-real set
|[X,B]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
uB is V28() real ext-real Element of REAL
|[uB,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
uB is V28() real ext-real Element of REAL
|[uB,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
len () is ordinal cardinal set
X is Relation-like Function-like set
proj1 X is set
proj2 X is set
B is set
uB is set
X . B is set
X . uB is set
V is V28() real ext-real Element of REAL
X . V is set
|[V,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
x is V28() real ext-real Element of REAL
X . x is set
|[x,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
B is set
uB is set
X . uB is set
x is V28() real ext-real Element of REAL
|[x,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
B is set
uB is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
uB `1 is V28() real ext-real Element of REAL
uB `2 is V28() real ext-real Element of REAL
|[(uB `1),(uB `2)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
X . (uB `1) is set
X is set
B is set
<*X,B*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*X,B*> . 1 is set
uB is V28() real ext-real Element of REAL
x is V28() real ext-real Element of REAL
|[uB,x]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
<*X,B*> . 2 is set
V is V28() real ext-real Element of REAL
x is V28() real ext-real Element of REAL
uB is V28() real ext-real Element of REAL
|[uB,x]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
X is V28() real ext-real set
B is V28() real ext-real set
|[X,B]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
uB is V28() real ext-real Element of REAL
x is V28() real ext-real Element of REAL
|[uB,x]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
uB is V28() real ext-real Element of REAL
x is V28() real ext-real Element of REAL
|[uB,x]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
X is set
B is Element of ()
B `1 is V28() real ext-real Element of REAL
B `2 is V28() real ext-real Element of REAL
|[(B `1),(B `2)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
uB is V28() real ext-real set
X is V28() real ext-real set
B is V28() real ext-real set
|[X,B]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Ball (|[X,B]|,uB) is Element of bool the carrier of (TOP-REAL 2)
x is V28() real ext-real non negative Element of REAL
x - uB is V28() real ext-real Element of REAL
V is non empty V28() real ext-real non positive negative Element of REAL
V / 2 is non empty V28() real ext-real non positive negative Element of REAL
|[X,(V / 2)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|[X,x]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|[X,(V / 2)]| - |[X,x]| is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(|[X,(V / 2)]|,|[X,x]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
X - X is V28() real ext-real set
(V / 2) - x is non empty V28() real ext-real non positive negative Element of REAL
|[(X - X),((V / 2) - x)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|.(|[X,(V / 2)]| - |[X,x]|).| is V28() real ext-real non negative Element of REAL
|.((V / 2) - x).| is V28() real ext-real Element of REAL
x - (V / 2) is non empty V28() real ext-real positive non negative Element of REAL
|.(x - (V / 2)).| is V28() real ext-real Element of REAL
x9 is non empty V28() real ext-real positive non negative Element of REAL
x + x9 is non empty V28() real ext-real positive non negative Element of REAL
(x + x9) / 2 is non empty V28() real ext-real positive non negative Element of REAL
x9 + x9 is non empty V28() real ext-real positive non negative Element of REAL
(x9 + x9) / 2 is non empty V28() real ext-real positive non negative Element of REAL
Ball (|[X,x]|,x9) is Element of bool the carrier of (TOP-REAL 2)
x is set
V is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
V - |[X,B]| is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(V,|[X,B]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(V - |[X,B]|).| is V28() real ext-real non negative Element of REAL
V `1 is V28() real ext-real Element of REAL
(V `1) - X is V28() real ext-real Element of REAL
V `2 is V28() real ext-real Element of REAL
(V `2) - B is V28() real ext-real Element of REAL
|[((V `1) - X),((V `2) - B)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|[((V `1) - X),((V `2) - B)]| `1 is V28() real ext-real Element of REAL
|[((V `1) - X),((V `2) - B)]| `2 is V28() real ext-real Element of REAL
|[(V `1),(V `2)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
((V `1) - X) ^2 is V28() real ext-real Element of REAL
((V `1) - X) * ((V `1) - X) is V28() real ext-real set
((V `2) - B) ^2 is V28() real ext-real Element of REAL
((V `2) - B) * ((V `2) - B) is V28() real ext-real set
(((V `1) - X) ^2) + (((V `2) - B) ^2) is V28() real ext-real Element of REAL
sqrt ((((V `1) - X) ^2) + (((V `2) - B) ^2)) is V28() real ext-real Element of REAL
abs ((V `2) - B) is V28() real ext-real Element of REAL
B - (V `2) is V28() real ext-real Element of REAL
abs (B - (V `2)) is V28() real ext-real Element of REAL
uB is V28() real ext-real set
B is V28() real ext-real set
X is V28() real ext-real set
|[X,B]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Ball (|[X,B]|,uB) is Element of bool the carrier of (TOP-REAL 2)
|[X,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|[X,0]| - |[X,B]| is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(|[X,0]|,|[X,B]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
X - X is V28() real ext-real set
0 - B is V28() real ext-real Element of REAL
|[(X - X),(0 - B)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|.(|[X,0]| - |[X,B]|).| is V28() real ext-real non negative Element of REAL
|.(0 - B).| is V28() real ext-real Element of REAL
B - 0 is V28() real ext-real Element of REAL
|.(B - 0).| is V28() real ext-real Element of REAL
x is set
V is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
V `1 is V28() real ext-real Element of REAL
V `2 is V28() real ext-real Element of REAL
|[(V `1),(V `2)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
V - |[X,B]| is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(V,|[X,B]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
(V `1) - X is V28() real ext-real Element of REAL
|[((V `1) - X),(0 - B)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
(V - |[X,B]|) `2 is V28() real ext-real Element of REAL
(V - |[X,B]|) `1 is V28() real ext-real Element of REAL
|.(V - |[X,B]|).| is V28() real ext-real non negative Element of REAL
((V `1) - X) ^2 is V28() real ext-real Element of REAL
((V `1) - X) * ((V `1) - X) is V28() real ext-real set
(0 - B) ^2 is V28() real ext-real Element of REAL
(0 - B) * (0 - B) is V28() real ext-real set
(((V `1) - X) ^2) + ((0 - B) ^2) is V28() real ext-real Element of REAL
sqrt ((((V `1) - X) ^2) + ((0 - B) ^2)) is V28() real ext-real Element of REAL
abs (0 - B) is V28() real ext-real Element of REAL
abs (B - 0) is V28() real ext-real Element of REAL
abs B is V28() real ext-real Element of REAL
X is ordinal natural V28() real ext-real finite cardinal V99() rational V169() V170() V171() V172() V173() V174() V269() V270() V271() Element of NAT
TOP-REAL X is non empty TopSpace-like V116() V181() V182() V241() V242() V243() V244() V245() V246() V247() V253() L16()
the carrier of (TOP-REAL X) is non empty set
B is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
uB is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
B - uB is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
K391(B,uB) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(B - uB).| is V28() real ext-real non negative Element of REAL
x is non empty V28() real ext-real positive non negative set
V is non empty V28() real ext-real positive non negative set
x - V is V28() real ext-real set
Ball (uB,V) is Element of bool the carrier of (TOP-REAL X)
bool the carrier of (TOP-REAL X) is non empty set
Ball (B,x) is Element of bool the carrier of (TOP-REAL X)
uB - B is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
K391(uB,B) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(uB - B).| is V28() real ext-real non negative Element of REAL
V9 is set
x9 is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
x9 - uB is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
K391(x9,uB) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(x9 - uB).| is V28() real ext-real non negative Element of REAL
V + (x - V) is V28() real ext-real set
|.(x9 - uB).| + |.(uB - B).| is V28() real ext-real non negative Element of REAL
x9 - B is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL X)
K391(x9,B) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(x9 - B).| is V28() real ext-real non negative Element of REAL
X is V28() real ext-real set
B is non empty V28() real ext-real positive non negative set
uB is non empty V28() real ext-real positive non negative set
|[X,B]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Ball (|[X,B]|,B) is Element of bool the carrier of (TOP-REAL 2)
|[X,uB]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Ball (|[X,uB]|,uB) is Element of bool the carrier of (TOP-REAL 2)
B - uB is V28() real ext-real set
uB - B is V28() real ext-real set
x is set
V is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
V - |[X,B]| is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(V,|[X,B]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(V - |[X,B]|).| is V28() real ext-real non negative Element of REAL
|[X,B]| - |[X,uB]| is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(|[X,B]|,|[X,uB]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
X - X is V28() real ext-real set
|[(X - X),(B - uB)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|.(|[X,B]| - |[X,uB]|).| is V28() real ext-real non negative Element of REAL
|.(B - uB).| is V28() real ext-real Element of REAL
|.(uB - B).| is V28() real ext-real Element of REAL
B + (uB - B) is V28() real ext-real set
|.(V - |[X,B]|).| + |.(|[X,B]| - |[X,uB]|).| is V28() real ext-real non negative Element of REAL
V - |[X,uB]| is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(V,|[X,uB]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(V - |[X,uB]|).| is V28() real ext-real non negative Element of REAL
X is non empty TopSpace-like TopStruct
the carrier of X is non empty set
B is non empty TopSpace-like TopStruct
the carrier of B is non empty set
the topology of X is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
TopStruct(# the carrier of X, the topology of X #) is non empty strict TopSpace-like TopStruct
the topology of B is non empty Element of bool (bool the carrier of B)
bool the carrier of B is non empty set
bool (bool the carrier of B) is non empty set
TopStruct(# the carrier of B, the topology of B #) is non empty strict TopSpace-like TopStruct
uB is Relation-like the carrier of X -defined Function-like total Neighborhood_System of X
x is Relation-like the carrier of B -defined Function-like total Neighborhood_System of B
dom uB is Element of bool the carrier of X
dom x is Element of bool the carrier of B
Union x is open quasi_basis Element of bool (bool the carrier of B)
UniCl (Union x) is Element of bool (bool the carrier of B)
Union uB is open quasi_basis Element of bool (bool the carrier of X)
UniCl (Union uB) is Element of bool (bool the carrier of X)
{ ((Ball (|[(a1 `1),b1]|,b1)) \/ {a1}) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
{ ((Ball (a1,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
B is Relation-like () -defined Function-like total set
uB is set
B . uB is set
the non empty V28() real ext-real positive non negative Element of REAL is non empty V28() real ext-real positive non negative Element of REAL
x is Element of ()
x `1 is V28() real ext-real Element of REAL
|[(x `1), the non empty V28() real ext-real positive non negative Element of REAL ]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
B . x is set
{x} is non empty trivial finite 1 -element Element of bool the carrier of (TOP-REAL 2)
{ ((Ball (|[(x `1),b1]|,b1)) \/ {x}) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
Ball (|[(x `1), the non empty V28() real ext-real positive non negative Element of REAL ]|, the non empty V28() real ext-real positive non negative Element of REAL ) is Element of bool the carrier of (TOP-REAL 2)
{x} is non empty trivial finite 1 -element Element of bool ()
bool () is non empty set
(Ball (|[(x `1), the non empty V28() real ext-real positive non negative Element of REAL ]|, the non empty V28() real ext-real positive non negative Element of REAL )) \/ {x} is set
the non empty V28() real ext-real positive non negative Element of REAL is non empty V28() real ext-real positive non negative Element of REAL
x is Element of ()
B . x is set
{ ((Ball (x,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
Ball (x, the non empty V28() real ext-real positive non negative Element of REAL ) is Element of bool the carrier of (TOP-REAL 2)
(Ball (x, the non empty V28() real ext-real positive non negative Element of REAL )) /\ () is Element of bool the carrier of (TOP-REAL 2)
uB is Relation-like non-empty () -defined Function-like total set
proj2 uB is with_non-empty_elements set
bool () is non empty Element of bool (bool ())
bool () is non empty set
bool (bool ()) is non empty set
bool (bool ()) is non empty Element of bool (bool (bool ()))
bool (bool ()) is non empty set
bool (bool (bool ())) is non empty set
x is set
dom uB is Element of bool ()
V is set
uB . V is set
x9 is set
V9 is Element of ()
V9 `1 is V28() real ext-real Element of REAL
{V9} is non empty trivial finite 1 -element Element of bool the carrier of (TOP-REAL 2)
{ ((Ball (|[(V9 `1),b1]|,b1)) \/ {V9}) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
{V9} is non empty trivial finite 1 -element Element of bool ()
r is V28() real ext-real Element of REAL
|[(V9 `1),r]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Ball (|[(V9 `1),r]|,r) is Element of bool the carrier of (TOP-REAL 2)
(Ball (|[(V9 `1),r]|,r)) \/ {V9} is set
V9 is Element of ()
{ ((Ball (V9,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
r is V28() real ext-real Element of REAL
Ball (V9,r) is Element of bool the carrier of (TOP-REAL 2)
(Ball (V9,r)) /\ () is Element of bool the carrier of (TOP-REAL 2)
V9 is Element of ()
V9 `1 is V28() real ext-real Element of REAL
{V9} is non empty trivial finite 1 -element Element of bool the carrier of (TOP-REAL 2)
{ ((Ball (|[(V9 `1),b1]|,b1)) \/ {V9}) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
{ ((Ball (V9,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
x is set
V9 is set
V is set
uB . V is set
uB . x is set
x9 is Element of ()
uB . x9 is set
x9 `1 is V28() real ext-real Element of REAL
{x9} is non empty trivial finite 1 -element Element of bool the carrier of (TOP-REAL 2)
{ ((Ball (|[(x9 `1),b1]|,b1)) \/ {x9}) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
{x9} is non empty trivial finite 1 -element Element of bool ()
r is V28() real ext-real Element of REAL
|[(x9 `1),r]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Ball (|[(x9 `1),r]|,r) is Element of bool the carrier of (TOP-REAL 2)
(Ball (|[(x9 `1),r]|,r)) \/ {x9} is set
f is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
f - |[(x9 `1),r]| is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(f,|[(x9 `1),r]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(f - |[(x9 `1),r]|).| is V28() real ext-real non negative Element of REAL
r - |.(f - |[(x9 `1),r]|).| is V28() real ext-real Element of REAL
Ball (f,(r - |.(f - |[(x9 `1),r]|).|)) is Element of bool the carrier of (TOP-REAL 2)
(Ball (f,(r - |.(f - |[(x9 `1),r]|).|))) /\ () is Element of bool the carrier of (TOP-REAL 2)
c is non empty V28() real ext-real positive non negative Element of REAL
uB . f is set
{ ((Ball (f,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
u is Element of bool the carrier of (TOP-REAL 2)
b is non empty V28() real ext-real positive non negative Element of REAL
b - c is V28() real ext-real Element of REAL
|[(x9 `1),r]| - f is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(|[(x9 `1),r]|,f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(|[(x9 `1),r]| - f).| is V28() real ext-real non negative Element of REAL
Ball (f,c) is Element of bool the carrier of (TOP-REAL 2)
Ball (|[(x9 `1),r]|,b) is Element of bool the carrier of (TOP-REAL 2)
f is Element of bool the carrier of (TOP-REAL 2)
x9 is Element of ()
uB . x9 is set
{ ((Ball (x9,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
r is V28() real ext-real Element of REAL
Ball (x9,r) is Element of bool the carrier of (TOP-REAL 2)
(Ball (x9,r)) /\ () is Element of bool the carrier of (TOP-REAL 2)
f is Element of ()
f - x9 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(f,x9) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(f - x9).| is V28() real ext-real non negative Element of REAL
r - |.(f - x9).| is V28() real ext-real Element of REAL
f `1 is V28() real ext-real Element of REAL
f `2 is V28() real ext-real Element of REAL
|[(f `1),(f `2)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
b is non empty V28() real ext-real positive non negative Element of REAL
b / 2 is non empty V28() real ext-real positive non negative Element of REAL
|[(f `1),(b / 2)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|[(f `1),(b / 2)]| - f is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(|[(f `1),(b / 2)]|,f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
(f `1) - (f `1) is V28() real ext-real Element of REAL
(b / 2) - 0 is V28() real ext-real Element of REAL
|[((f `1) - (f `1)),((b / 2) - 0)]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
|.(|[(f `1),(b / 2)]| - f).| is V28() real ext-real non negative Element of REAL
abs (b / 2) is V28() real ext-real Element of REAL
|[(f `1),(b / 2)]| - x9 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(|[(f `1),(b / 2)]|,x9) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(|[(f `1),(b / 2)]| - x9).| is V28() real ext-real non negative Element of REAL
(b / 2) + |.(f - x9).| is non empty V28() real ext-real positive non negative Element of REAL
x9 - |[(f `1),(b / 2)]| is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(x9,|[(f `1),(b / 2)]|) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(x9 - |[(f `1),(b / 2)]|).| is V28() real ext-real non negative Element of REAL
r - (b / 2) is V28() real ext-real Element of REAL
Ball (|[(f `1),(b / 2)]|,(b / 2)) is Element of bool the carrier of (TOP-REAL 2)
u is non empty V28() real ext-real positive non negative Element of REAL
Ball (x9,u) is Element of bool the carrier of (TOP-REAL 2)
{f} is non empty trivial finite 1 -element Element of bool ()
(Ball (|[(f `1),(b / 2)]|,(b / 2))) \/ {f} is set
uB . f is set
{f} is non empty trivial finite 1 -element Element of bool the carrier of (TOP-REAL 2)
{ ((Ball (|[(f `1),b1]|,b1)) \/ {f}) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
b is non empty V28() real ext-real positive non negative Element of REAL
Ball (f,b) is Element of bool the carrier of (TOP-REAL 2)
(Ball (f,b)) /\ () is Element of bool the carrier of (TOP-REAL 2)
c is Element of bool the carrier of (TOP-REAL 2)
uB . f is set
{ ((Ball (f,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
x9 - f is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
K391(x9,f) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V159() V160() V161() FinSequence of REAL
|.(x9 - f).| is V28() real ext-real non negative Element of REAL
u is non empty V28() real ext-real positive non negative Element of REAL
u - b is V28() real ext-real Element of REAL
x9 is Element of ()
x is set
V is set
uB . x is set
V9 is set
V /\ V9 is set
x9 is Element of ()
x9 `1 is V28() real ext-real Element of REAL
{x9} is non empty trivial finite 1 -element Element of bool the carrier of (TOP-REAL 2)
{ ((Ball (|[(x9 `1),b1]|,b1)) \/ {x9}) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
{x9} is non empty trivial finite 1 -element Element of bool ()
r is V28() real ext-real Element of REAL
|[(x9 `1),r]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Ball (|[(x9 `1),r]|,r) is Element of bool the carrier of (TOP-REAL 2)
(Ball (|[(x9 `1),r]|,r)) \/ {x9} is set
f is V28() real ext-real Element of REAL
|[(x9 `1),f]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Ball (|[(x9 `1),f]|,f) is Element of bool the carrier of (TOP-REAL 2)
(Ball (|[(x9 `1),f]|,f)) \/ {x9} is set
f is set
x9 is Element of ()
{ ((Ball (x9,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
r is V28() real ext-real Element of REAL
Ball (x9,r) is Element of bool the carrier of (TOP-REAL 2)
(Ball (x9,r)) /\ () is Element of bool the carrier of (TOP-REAL 2)
f is V28() real ext-real Element of REAL
Ball (x9,f) is Element of bool the carrier of (TOP-REAL 2)
(Ball (x9,f)) /\ () is Element of bool the carrier of (TOP-REAL 2)
f is set
x9 is Element of ()
x is set
V is set
uB . x is set
V9 is Element of ()
V9 `1 is V28() real ext-real Element of REAL
{V9} is non empty trivial finite 1 -element Element of bool the carrier of (TOP-REAL 2)
{ ((Ball (|[(V9 `1),b1]|,b1)) \/ {V9}) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
{V9} is non empty trivial finite 1 -element Element of bool ()
x9 is V28() real ext-real Element of REAL
|[(V9 `1),x9]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
Ball (|[(V9 `1),x9]|,x9) is Element of bool the carrier of (TOP-REAL 2)
(Ball (|[(V9 `1),x9]|,x9)) \/ {V9} is set
V9 is Element of ()
{ ((Ball (V9,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
x9 is V28() real ext-real Element of REAL
Ball (V9,x9) is Element of bool the carrier of (TOP-REAL 2)
(Ball (V9,x9)) /\ () is Element of bool the carrier of (TOP-REAL 2)
V9 is Element of ()
V9 `1 is V28() real ext-real Element of REAL
{V9} is non empty trivial finite 1 -element Element of bool the carrier of (TOP-REAL 2)
{ ((Ball (|[(V9 `1),b1]|,b1)) \/ {V9}) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
{ ((Ball (V9,b1)) /\ ()) where b1 is V28() real ext-real Element of REAL : not b1 <= 0 } is set
Union uB is set
x is Element of bool (bool ())
UniCl x is Element of bool (bool ())
TopStruct(# (),(UniCl x) #) is non empty strict TopStruct
V9 is non empty strict TopSpace-like TopStruct
the carrier of V9 is non empty set
x9 is Relation-like the carrier of V9 -defined Function-like total Neighborhood_System of V9
r is V28() real ext-real Element of REAL
|[r,0]| is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like V159() V160() V161() Element of the carrier of (TOP-REAL 2)
{|[r,0]|} is functional non empty trivial finite V37() 1 -element Element of bool the carrier of (TOP-REAL 2)
|[r,0]| `1 is V28() real ext-real Element of REAL
f is V28() real ext-real