:: TOPGEN_5 semantic presentation

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

{ [.b

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

F

F

F

[:F

bool [:F

X is set

F

F

X is Relation-like F

B is Element of F

X . B is set

F

F

F

F

F

[:F

bool [:F

{ b

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

F

uB is Relation-like F

x is Element of F

uB . x is set

F

F

F

B is non empty set

uB is set

F

F

x is Element of F

x is Element of F

[:B,F

bool [:B,F

uB is Relation-like B -defined F

x is set

uB . x is set

F

F

F

x is Relation-like F

V is Element of F

x . V is set

F

F

F

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

{ |[b

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)

{ |[b

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 (|[(a

{ ((Ball (a

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),b

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,b

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),b

{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,b

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),b

{ ((Ball (V9,b

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),b

{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,b

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,b

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),b

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,b

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),b

{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,b

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),b

{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,b

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),b

{ ((Ball (V9,b

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