:: NAGATA_1 semantic presentation

REAL is non empty non trivial non finite V130() V131() V132() V136() set
NAT is non empty non trivial non finite countable denumerable V130() V131() V132() V133() V134() V135() V136() Element of bool REAL
bool REAL is non empty set
K490() is V130() V131() V132() Element of bool REAL
omega is non empty non trivial non finite countable denumerable V130() V131() V132() V133() V134() V135() V136() set
bool omega is non empty set
is non empty V119() V120() V121() set
bool is non empty set
bool () is non empty set
bool NAT is non empty set
K96(NAT) is V24() set
COMPLEX is non empty non trivial non finite V130() V136() set
1 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
INT is non empty non trivial non finite V130() V131() V132() V133() V134() V136() set
[:1,1:] is RAT -valued INT -valued non empty V119() V120() V121() V122() set
RAT is non empty non trivial non finite V130() V131() V132() V133() V136() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is RAT -valued INT -valued non empty V119() V120() V121() V122() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V119() V120() V121() set
bool [:[:1,1:],REAL:] is non empty set
is non empty V119() V120() V121() set
is non empty V119() V120() V121() set
bool is non empty set
2 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
[:2,2:] is RAT -valued INT -valued non empty V119() V120() V121() V122() set
[:[:2,2:],REAL:] is non empty V119() V120() V121() set
bool [:[:2,2:],REAL:] is non empty set
bool is non empty set
K456(2) is V190() L15()
the carrier of K456(2) is set
[: the carrier of K456(2),REAL:] is V119() V120() V121() set
bool [: the carrier of K456(2),REAL:] is non empty set
bool the carrier of K456(2) is non empty set
K550() is non empty strict TopSpace-like V213() TopStruct
the carrier of K550() is non empty V130() V131() V132() set

R^1 is non empty strict TopSpace-like V213() TopStruct
K491() is V130() V131() V132() Element of bool REAL
ExtREAL is non empty V131() set
bool ExtREAL is non empty set
the carrier of R^1 is non empty V130() V131() V132() set

3 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT

the carrier of RealSpace is non empty V130() V131() V132() set

Family_open_set RealSpace is Element of bool (bool the carrier of RealSpace)
bool the carrier of RealSpace is non empty set
bool (bool the carrier of RealSpace) is non empty set
TopStruct(# the carrier of RealSpace, #) is non empty strict TopStruct

T is V33() real ext-real Element of REAL
r is V33() real ext-real Element of REAL
m is V33() real ext-real Element of REAL
T + r is V33() real ext-real Element of REAL
m + 0 is V33() real ext-real Element of REAL
r + T is V33() real ext-real Element of REAL
T is V33() real ext-real Element of REAL
a is V33() real ext-real Element of REAL
T - a is V33() real ext-real Element of REAL
abs (T - a) is V33() real ext-real Element of REAL
r is V33() real ext-real Element of REAL
T - r is V33() real ext-real Element of REAL
abs (T - r) is V33() real ext-real Element of REAL
m is V33() real ext-real Element of REAL
r - m is V33() real ext-real Element of REAL
abs (r - m) is V33() real ext-real Element of REAL
(abs (T - r)) + (abs (r - m)) is V33() real ext-real Element of REAL
m - a is V33() real ext-real Element of REAL
abs (m - a) is V33() real ext-real Element of REAL
((abs (T - r)) + (abs (r - m))) + (abs (m - a)) is V33() real ext-real Element of REAL
r - a is V33() real ext-real Element of REAL
(r - m) + (m - a) is V33() real ext-real Element of REAL
abs (r - a) is V33() real ext-real Element of REAL
(abs (r - m)) + (abs (m - a)) is V33() real ext-real Element of REAL
(abs (T - r)) + (abs (r - a)) is V33() real ext-real Element of REAL
(abs (T - r)) + ((abs (r - m)) + (abs (m - a))) is V33() real ext-real Element of REAL
(T - r) + (r - a) is V33() real ext-real Element of REAL

the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{. the carrier of T,.} is non empty finite countable set
m is set
m is Element of bool (bool the carrier of T)
a is Element of the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
b is non empty non proper open closed Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
b /\ c is Element of bool the carrier of T
b /\ ft is Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
a is Element of bool the carrier of T
b is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool the carrier of T
{m} is non empty trivial finite countable Element of bool (bool the carrier of T)
m is Element of bool the carrier of T
{m} is non empty trivial finite countable Element of bool (bool the carrier of T)
[#] T is non empty non proper open closed Element of bool the carrier of T
a is Element of the carrier of T
b is non empty non proper open closed Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
{c} is non empty trivial finite countable Element of bool (bool the carrier of T)
{ft} is non empty trivial finite countable Element of bool (bool the carrier of T)
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
a is Element of the carrier of T
b is open Element of bool the carrier of T
c is open Element of bool the carrier of T
ft is Element of bool the carrier of T
R is Element of bool the carrier of T
b is open Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
r /\ m is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
r \ m is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
INTERSECTION (r,m) is set
a is Element of bool (bool the carrier of T)
b is Element of the carrier of T
c is open Element of bool the carrier of T
ft is open Element of bool the carrier of T
R is Element of bool the carrier of T
s is Element of bool the carrier of T
B is set
U is set
B /\ U is set
c /\ ft is open Element of bool the carrier of T
mfx is set
x is set
mfx /\ x is set
(c /\ ft) /\ (mfx /\ x) is Element of bool the carrier of T
(c /\ ft) /\ mfx is Element of bool the carrier of T
((c /\ ft) /\ mfx) /\ x is Element of bool the carrier of T
c /\ mfx is Element of bool the carrier of T
(c /\ mfx) /\ ft is Element of bool the carrier of T
((c /\ mfx) /\ ft) /\ x is Element of bool the carrier of T
(c /\ ft) /\ (B /\ U) is Element of bool the carrier of T
(c /\ ft) /\ B is Element of bool the carrier of T
((c /\ ft) /\ B) /\ U is Element of bool the carrier of T
c /\ B is Element of bool the carrier of T
(c /\ B) /\ ft is Element of bool the carrier of T
((c /\ B) /\ ft) /\ U is Element of bool the carrier of T
ft /\ U is Element of bool the carrier of T
(c /\ B) /\ (ft /\ U) is Element of bool the carrier of T
ft /\ x is Element of bool the carrier of T
(c /\ mfx) /\ (ft /\ x) is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool the carrier of T
a is Element of bool the carrier of T
m /\ a is Element of bool the carrier of T

b is Element of the carrier of T
c is open Element of bool the carrier of T
{b} is non empty trivial finite countable compact Element of bool the carrier of T
c /\ a is Element of bool the carrier of T
c /\ m is Element of bool the carrier of T
is non empty trivial finite V45() countable set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of the carrier of T
a is open Element of bool the carrier of T
{a} is non empty trivial finite countable Element of bool (bool the carrier of T)
INTERSECTION ({a},r) is set
c is set
ft is set
R is set
s is set
R /\ s is set
B is set
U is set
B /\ U is set

c is set
{.c,.} is non empty finite countable set
ft is set
(INTERSECTION ({a},r)) \ is Element of bool (INTERSECTION ({a},r))
bool (INTERSECTION ({a},r)) is non empty set
c is set
{.c,.} is non empty finite countable set
ft is set

(INTERSECTION ({a},r)) \ is Element of bool (INTERSECTION ({a},r))
bool (INTERSECTION ({a},r)) is non empty set
(INTERSECTION ({a},r)) \ is Element of bool (INTERSECTION ({a},r))
bool (INTERSECTION ({a},r)) is non empty set
(INTERSECTION ({a},r)) \ is Element of bool (INTERSECTION ({a},r))
bool (INTERSECTION ({a},r)) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
a is Element of the carrier of T
b is open Element of bool the carrier of T
{b} is non empty trivial finite countable Element of bool (bool the carrier of T)
INTERSECTION ({b},m) is set
(INTERSECTION ({b},m)) \ is Element of bool (INTERSECTION ({b},m))
bool (INTERSECTION ({b},m)) is non empty set
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
b /\ ft is Element of bool the carrier of T
s is set

{(b /\ ft)} is non empty trivial finite countable Element of bool (bool the carrier of T)
b /\ c is Element of bool the carrier of T
B is set
{(b /\ c)} is non empty trivial finite countable Element of bool (bool the carrier of T)
c /\ ft is Element of bool the carrier of T
a is Element of the carrier of T
b is Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of the carrier of T
R is Element of bool the carrier of T
s is Element of bool the carrier of T
m is Element of the carrier of T
a is Element of bool the carrier of T
b is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
r is open Element of bool the carrier of T
m is Element of bool the carrier of T
Cl m is closed Element of bool the carrier of T
r ` is closed Element of bool the carrier of T
the carrier of T \ r is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is (T) Element of bool (bool the carrier of T)
clf r is Element of bool (bool the carrier of T)
m is Element of the carrier of T
a is open Element of bool the carrier of T
b is Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
Cl ft is closed Element of bool the carrier of T
R is Element of bool the carrier of T
Cl R is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
union r is Element of bool the carrier of T
Cl () is closed Element of bool the carrier of T
m is Element of bool the carrier of T
Cl m is closed Element of bool the carrier of T
a is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool the carrier of T
Cl m is closed Element of bool the carrier of T
a is Element of bool the carrier of T
m /\ a is Element of bool the carrier of T
Cl (m /\ a) is closed Element of bool the carrier of T
Cl a is closed Element of bool the carrier of T
(Cl m) /\ (Cl a) is closed Element of bool the carrier of T

b is set
c is open Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
union r is Element of bool the carrier of T
Cl () is closed Element of bool the carrier of T
clf r is Element of bool (bool the carrier of T)
union (clf r) is Element of bool the carrier of T
m is set
a is open Element of bool the carrier of T
b is set
c is set
ft is Element of bool the carrier of T
R is Element of bool the carrier of T
R is Element of bool the carrier of T
R /\ a is Element of bool the carrier of T
s is set
B is set
R /\ B is Element of bool the carrier of T
a /\ B is Element of bool the carrier of T
Cl ft is closed Element of bool the carrier of T
m is set
a is set
b is Element of bool the carrier of T
c is Element of bool the carrier of T
Cl c is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of the carrier of T
a is open Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in r & not b1 misses a ) } is set
c is open Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in r & not b1 misses c ) } is set
ft is set
R is Element of bool the carrier of T
s is set
B is Element of bool the carrier of T
{R} is non empty trivial finite countable Element of bool (bool the carrier of T)
ft is Element of bool the carrier of T
{ft} is non empty trivial finite countable Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
m is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r . m is set
r . m is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Union r is set
Union r is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set

is non empty trivial finite V45() countable set
is non empty set
bool is non empty set
m is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
a is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,m,a) is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
T is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
m is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,r,m) is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
m is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,r,m) is Element of bool (bool the carrier of T)
T is non empty non countable set
[:T,T:] is non empty set
1TopSp [:T,T:] is non empty strict TopSpace-like TopStruct
bool [:T,T:] is non empty Element of bool (bool [:T,T:])
bool [:T,T:] is non empty set
bool (bool [:T,T:]) is non empty set
[#] (bool [:T,T:]) is non empty non proper Element of bool (bool [:T,T:])
bool (bool [:T,T:]) is non empty set
TopStruct(# [:T,T:],([#] (bool [:T,T:])) #) is non empty strict TopStruct
the carrier of (1TopSp [:T,T:]) is non empty set
bool the carrier of (1TopSp [:T,T:]) is non empty set
bool (bool the carrier of (1TopSp [:T,T:])) is non empty set
{ ([:{b1},T:] \/ [:T,{b1}:]) where b1 is Element of T : b1 in T } is set
a is set
b is Element of T
{b} is non empty trivial finite countable Element of bool T
bool T is non empty set
[:{b},T:] is non empty set
[:T,{b}:] is non empty set
[:{b},T:] \/ [:T,{b}:] is non empty set
a is Element of bool (bool the carrier of (1TopSp [:T,T:]))
b is Element of the carrier of (1TopSp [:T,T:])
{b} is non empty trivial finite countable compact Element of bool the carrier of (1TopSp [:T,T:])
R is set
s is set
[R,s] is non empty set
{.s,.} is non empty finite countable set

is non empty finite V45() countable set

[:,T:] is non empty set
[:T,:] is non empty set
[:,T:] \/ [:T,:] is non empty set

[:,T:] is non empty set
[:T,:] is non empty set
[:,T:] \/ [:T,:] is non empty set

ft is Element of bool the carrier of (1TopSp [:T,T:])
{ b1 where b1 is Element of bool the carrier of (1TopSp [:T,T:]) : ( b1 in a & not b1 misses ft ) } is set

x is set
x is Element of bool the carrier of (1TopSp [:T,T:])
fx is set
fx is Element of T
{fx} is non empty trivial finite countable Element of bool T
bool T is non empty set
[:{fx},T:] is non empty set
[:T,{fx}:] is non empty set
[:{fx},T:] \/ [:T,{fx}:] is non empty set
b is set
c is Element of T
{c} is non empty trivial finite countable Element of bool T
bool T is non empty set
[:{c},T:] is non empty set
[:T,{c}:] is non empty set
[:{c},T:] \/ [:T,{c}:] is non empty set

dom R is set
s is set
B is set
R . s is set
R . B is set

[s,s] is non empty set
{.s,.} is non empty finite countable set
is non empty finite V45() countable set
[:,T:] is non empty set
[:T,:] is non empty set
[:,T:] \/ [:T,:] is non empty set

[:,T:] is non empty set
[:T,:] is non empty set
[:,T:] \/ [:T,:] is non empty set
rng R is set
s is set
B is set
R . B is set
U is Element of T
{U} is non empty trivial finite countable Element of bool T
[:{U},T:] is non empty set
[:T,{U}:] is non empty set
[:{U},T:] \/ [:T,{U}:] is non empty set
[:NAT,(bool (bool the carrier of (1TopSp [:T,T:]))):] is non empty set
bool [:NAT,(bool (bool the carrier of (1TopSp [:T,T:]))):] is non empty set
R is Relation-like NAT -defined bool (bool the carrier of (1TopSp [:T,T:])) -valued Function-like non empty V14( NAT ) quasi_total ( 1TopSp [:T,T:]) Element of bool [:NAT,(bool (bool the carrier of (1TopSp [:T,T:]))):]
((1TopSp [:T,T:]),R) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
s is set
R . s is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
((1TopSp [:T,T:]),R,B) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
R . B is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
((1TopSp [:T,T:]),R,B) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
U is set
R . B is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
((1TopSp [:T,T:]),R,B) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
R . B is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R . B is set
U is set
[:NAT,a:] is set
bool [:NAT,a:] is non empty set

B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R . B is set
U is Element of a
mfx is Element of a
((1TopSp [:T,T:]),R,B) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
x is Element of T
{x} is non empty trivial finite countable Element of bool T
[:{x},T:] is non empty set
[:T,{x}:] is non empty set
[:{x},T:] \/ [:T,{x}:] is non empty set
x is Element of T
{x} is non empty trivial finite countable Element of bool T
[:{x},T:] is non empty set
[:T,{x}:] is non empty set
[:{x},T:] \/ [:T,{x}:] is non empty set
[x,x] is non empty Element of [:T,T:]
{.x,.} is non empty finite countable set

is non empty finite V45() countable set
s .: NAT is Element of bool a
bool a is non empty set
B is set
U is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
((1TopSp [:T,T:]),R,U) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
s . U is Element of a
R . U is set
dom s is countable V130() V131() V132() V133() V134() V135() Element of bool NAT

len () is cardinal set
a \ () is Element of bool (bool the carrier of (1TopSp [:T,T:]))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is V33() real ext-real set

the carrier of m is non empty set
[#] m is non empty non proper Element of bool the carrier of m
bool the carrier of m is non empty set
Family_open_set m is Element of bool (bool the carrier of m)
bool (bool the carrier of m) is non empty set
a is Element of the carrier of m
cl_Ball (a,T) is Element of bool the carrier of m
([#] m) \ (cl_Ball (a,T)) is Element of bool the carrier of m
b is Element of the carrier of m
dist (a,b) is V33() real ext-real Element of REAL
r is V33() real ext-real Element of REAL
(dist (a,b)) - r is V33() real ext-real Element of REAL
Ball (b,((dist (a,b)) - r)) is Element of bool the carrier of m
ft is set
R is Element of the carrier of m
dist (a,R) is V33() real ext-real Element of REAL
dist (b,R) is V33() real ext-real Element of REAL
((dist (a,b)) - r) + r is V33() real ext-real Element of REAL
(dist (b,R)) + (dist (a,R)) is V33() real ext-real Element of REAL
dist (R,b) is V33() real ext-real Element of REAL
(dist (a,R)) + (dist (R,b)) is V33() real ext-real Element of REAL
r + ((dist (a,b)) - r) is V33() real ext-real Element of REAL
r + 0 is V33() real ext-real Element of REAL
((dist (a,b)) - r) - 0 is V33() real ext-real Element of REAL
r - r is V33() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
the topology of T is non empty open Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty V14([: the carrier of T, the carrier of T:]) quasi_total V119() V120() V121() Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

Family_open_set (SpaceMetr ( the carrier of T,r)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of T,r)))
the carrier of (SpaceMetr ( the carrier of T,r)) is set
bool the carrier of (SpaceMetr ( the carrier of T,r)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of T,r))) is non empty set

the carrier of a is non empty set
Family_open_set a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
TopStruct(# the carrier of a,() #) is non empty strict TopStruct
c is Element of the carrier of T
ft is Element of bool the carrier of T
ft ` is Element of bool the carrier of T
the carrier of T \ ft is set
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) \ ft is Element of bool the carrier of T
the carrier of () is set
bool the carrier of () is non empty set
[#] () is non proper Element of bool the carrier of ()
s is Element of bool the carrier of ()
([#] ()) \ s is Element of bool the carrier of ()
R is Element of the carrier of a
B is Element of bool the carrier of ()
U is V33() real ext-real Element of REAL
Ball (R,U) is Element of bool the carrier of a
mfx is set
Cl s is Element of bool the carrier of ()
B is V33() real ext-real Element of REAL
Ball (R,B) is Element of bool the carrier of a
B is V33() real ext-real Element of REAL
Ball (R,B) is Element of bool the carrier of a
B / 2 is V33() real ext-real Element of REAL
(B / 2) + (B / 2) is V33() real ext-real Element of REAL
[#] a is non empty non proper Element of bool the carrier of a
cl_Ball (R,(B / 2)) is Element of bool the carrier of a
([#] a) \ (cl_Ball (R,(B / 2))) is Element of bool the carrier of a
mfx is set
x is Element of the carrier of a
dist (R,x) is V33() real ext-real Element of REAL
(B / 2) / 2 is V33() real ext-real Element of REAL
((B / 2) / 2) + ((B / 2) / 2) is V33() real ext-real Element of REAL
Ball (R,((B / 2) / 2)) is Element of bool the carrier of a
x is set
x is Element of the carrier of a
dist (R,x) is V33() real ext-real Element of REAL
fx is Element of bool the carrier of T
fx is Element of bool the carrier of T
dist (R,R) is V33() real ext-real Element of REAL
c is Element of the carrier of T
ft is Element of the carrier of T
the carrier of () is set
bool the carrier of () is non empty set
R is Element of the carrier of ()
s is Element of the carrier of ()
B is Element of bool the carrier of ()
U is Element of bool the carrier of ()
mfx is Element of bool the carrier of T
x is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
the topology of T is non empty open Element of bool (bool the carrier of T)
r is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty V14([: the carrier of T, the carrier of T:]) quasi_total V119() V120() V121() Element of bool [:[: the carrier of T, the carrier of T:],REAL:]

Family_open_set (SpaceMetr ( the carrier of T,r)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of T,r)))
the carrier of (SpaceMetr ( the carrier of T,r)) is set
bool the carrier of (SpaceMetr ( the carrier of T,r)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of T,r))) is non empty set

the carrier of a is non empty set
{ (Ball (b1,(1 / (2 |^ a1)))) where b1 is Element of the carrier of a : b1 is Element of the carrier of a } is set
b is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
2 |^ b is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ b) is V33() real ext-real non negative Element of REAL
{ (Ball (b1,(1 / (2 |^ b)))) where b1 is Element of the carrier of a : b1 is Element of the carrier of a } is set
ft is set
Family_open_set a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
R is Element of the carrier of a
Ball (R,(1 / (2 |^ b))) is Element of bool the carrier of a
b is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]

Family_open_set a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
TopStruct(# the carrier of a,() #) is non empty strict TopStruct
[#] T is non empty non proper open closed Element of bool the carrier of T
[#] () is non proper Element of bool the carrier of ()
the carrier of () is set
bool the carrier of () is non empty set
ft is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,b,ft) is Element of bool (bool the carrier of T)
union (T,b,ft) is Element of bool the carrier of T
R is set
s is Element of the carrier of a
dist (s,s) is V33() real ext-real Element of REAL
2 |^ ft is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ ft) is V33() real ext-real non negative Element of REAL
Ball (s,(1 / (2 |^ ft))) is Element of bool the carrier of a
{ (Ball (b1,(1 / (2 |^ ft)))) where b1 is Element of the carrier of a : b1 is Element of the carrier of a } is set
R is Element of bool the carrier of T
2 |^ ft is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ ft) is V33() real ext-real non negative Element of REAL
{ (Ball (b1,(1 / (2 |^ ft)))) where b1 is Element of the carrier of a : b1 is Element of the carrier of a } is set
s is Element of the carrier of a
Ball (s,(1 / (2 |^ ft))) is Element of bool the carrier of a
R is Element of bool (bool the carrier of T)
ft is set
b . ft is set
R is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,b,R) is Element of bool (bool the carrier of T)
s is Element of bool (bool the carrier of T)
ft is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
(T,ft) is Element of bool (bool the carrier of T)
R is Element of bool the carrier of T
s is Element of the carrier of T
B is Element of the carrier of a
U is V33() real ext-real Element of REAL
Ball (B,U) is Element of bool the carrier of a
mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
2 |^ mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ mfx) is V33() real ext-real non negative Element of REAL
mfx + 1 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,ft,(mfx + 1)) is Element of bool (bool the carrier of T)
b . (mfx + 1) is set
union (T,ft,(mfx + 1)) is Element of bool the carrier of T
x is Element of bool (bool the carrier of T)
x is set
(T,b,(mfx + 1)) is Element of bool (bool the carrier of T)
x is Element of bool the carrier of a
fx is Element of bool (bool the carrier of T)
fx is set
2 |^ (mfx + 1) is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ (mfx + 1)) is V33() real ext-real non negative Element of REAL
{ (Ball (b1,(1 / (2 |^ (mfx + 1))))) where b1 is Element of the carrier of a : b1 is Element of the carrier of a } is set
fx is Element of the carrier of a
Ball (fx,(1 / (2 |^ (mfx + 1)))) is Element of bool the carrier of a
dist (fx,B) is V33() real ext-real Element of REAL
r9 is Element of the carrier of a
dist (fx,r9) is V33() real ext-real Element of REAL
dist (B,r9) is V33() real ext-real Element of REAL
(dist (fx,B)) + (dist (fx,r9)) is V33() real ext-real Element of REAL
(1 / (2 |^ (mfx + 1))) + (1 / (2 |^ (mfx + 1))) is V33() real ext-real non negative Element of REAL
2 * (1 / (2 |^ (mfx + 1))) is V33() real ext-real non negative Element of REAL
(2 |^ mfx) * 2 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / ((2 |^ mfx) * 2) is V33() real ext-real non negative Element of REAL
(1 / ((2 |^ mfx) * 2)) * 2 is V33() real ext-real non negative Element of REAL
R is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,ft,R) is Element of bool (bool the carrier of T)
b . R is set
s is Element of bool (bool the carrier of T)
R is set
s is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,ft,s) is Element of bool (bool the carrier of T)
b . s is set
B is Element of bool the carrier of T
U is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
r is open Element of bool the carrier of T
m is Element of bool the carrier of T
r \ m is Element of bool the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) \ m is Element of bool the carrier of T
r /\ (([#] T) \ m) is Element of bool the carrier of T
m ` is Element of bool the carrier of T
the carrier of T \ m is set
r /\ (m `) is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
[:NAT,(bool the carrier of T):] is non empty set
bool [:NAT,(bool the carrier of T):] is non empty set
r is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
Union r is Element of bool the carrier of T
rng r is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
the topology of T is non empty open Element of bool (bool the carrier of T)
m is set
dom r is countable V130() V131() V132() V133() V134() V135() Element of bool NAT
a is set
r . a is set
b is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r . b is Element of bool the carrier of T
union (rng r) is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
[:NAT,(bool the carrier of T):] is non empty set
bool [:NAT,(bool the carrier of T):] is non empty set
r is Element of bool the carrier of T
m is Element of bool the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) \ m is Element of bool the carrier of T
m ` is Element of bool the carrier of T
the carrier of T \ m is set
b is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
Union b is Element of bool the carrier of T
([#] T) \ r is Element of bool the carrier of T
r ` is Element of bool the carrier of T
the carrier of T \ r is set
ft is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
Union ft is Element of bool the carrier of T
is non empty trivial finite V45() countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg a1) \/ } is set
union { (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg a1) \/ } is set
R is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . R is Element of bool the carrier of T
Seg R is finite R -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg R) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg R) \/ } is set
union { (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg R) \/ } is set
(ft . R) \ (union { (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg R) \/ } ) is Element of bool the carrier of T
R is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
s is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R . s is Element of bool the carrier of T
Seg s is finite s -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg s) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg s) \/ } is set
U is set
mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . mfx is Element of bool the carrier of T
Cl (b . mfx) is closed Element of bool the carrier of T
bool (bool the carrier of T) is non empty set
{ H2(b1) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg s) \/ } is set
mfx is Element of bool the carrier of T
U is Element of bool (bool the carrier of T)
x is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . x is Element of bool the carrier of T
Cl (b . x) is closed Element of bool the carrier of T
ft . s is Element of bool the carrier of T
union U is Element of bool the carrier of T
(ft . s) \ () is Element of bool the carrier of T
Union R is Element of bool the carrier of T
s is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . s is Element of bool the carrier of T
Cl (b . s) is closed Element of bool the carrier of T
s is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . B is Element of bool the carrier of T
Seg B is finite B -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg B) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg B) \/ } is set
union { (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg B) \/ } is set
U is set
mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . mfx is Element of bool the carrier of T
Cl (b . mfx) is closed Element of bool the carrier of T
(ft . B) \ (union { (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg B) \/ } ) is Element of bool the carrier of T
R . B is Element of bool the carrier of T
{ (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg a1) \/ } is set
union { (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg a1) \/ } is set
s is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . s is Element of bool the carrier of T
Seg s is finite s -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg s) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg s) \/ } is set
union { (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg s) \/ } is set
(b . s) \ (union { (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg s) \/ } ) is Element of bool the carrier of T
s is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
Union s is Element of bool the carrier of T
B is set
U is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R . U is Element of bool the carrier of T
mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
s . mfx is Element of bool the carrier of T
x is set
b . mfx is Element of bool the carrier of T
Seg mfx is finite mfx -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg mfx) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg mfx) \/ } is set
union { (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg mfx) \/ } is set
(b . mfx) \ (union { (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg mfx) \/ } ) is Element of bool the carrier of T
Seg U is finite U -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg U) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
Cl (b . mfx) is closed Element of bool the carrier of T
{ (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg U) \/ } is set
ft . U is Element of bool the carrier of T
union { (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg U) \/ } is set
(ft . U) \ (union { (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg U) \/ } ) is Element of bool the carrier of T
x is set
ft . U is Element of bool the carrier of T
Seg U is finite U -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg U) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg U) \/ } is set
union { (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg U) \/ } is set
(ft . U) \ (union { (Cl (b . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg U) \/ } ) is Element of bool the carrier of T
Seg mfx is finite mfx -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg mfx) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
Cl (ft . U) is closed Element of bool the carrier of T
{ (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg mfx) \/ } is set
b . mfx is Element of bool the carrier of T
union { (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg mfx) \/ } is set
(b . mfx) \ (union { (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg mfx) \/ } ) is Element of bool the carrier of T
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
s . B is Element of bool the carrier of T
Seg B is finite B -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg B) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg B) \/ } is set
mfx is set
x is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . x is Element of bool the carrier of T
Cl (ft . x) is closed Element of bool the carrier of T
bool (bool the carrier of T) is non empty set
{ H3(b1) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg B) \/ } is set
x is Element of bool the carrier of T
mfx is Element of bool (bool the carrier of T)
x is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . x is Element of bool the carrier of T
Cl (ft . x) is closed Element of bool the carrier of T
b . B is Element of bool the carrier of T
union mfx is Element of bool the carrier of T
(b . B) \ (union mfx) is Element of bool the carrier of T
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . B is Element of bool the carrier of T
Cl (ft . B) is closed Element of bool the carrier of T
B is set
U is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . U is Element of bool the carrier of T
Seg U is finite U -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg U) \/ is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg U) \/ } is set
union { (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg U) \/ } is set
mfx is set
x is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . x is Element of bool the carrier of T
Cl (ft . x) is closed Element of bool the carrier of T
(b . U) \ (union { (Cl (ft . b1)) where b1 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b1 in (Seg U) \/ } ) is Element of bool the carrier of T
s . U is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
(T,r) is Element of bool (bool the carrier of T)
m is open Element of bool the carrier of T
a is Element of the carrier of T
b is Element of bool the carrier of T
c is Element of bool the carrier of T
Cl c is closed Element of bool the carrier of T
m ` is closed Element of bool the carrier of T
the carrier of T \ m is set
(m `) ` is open Element of bool the carrier of T
the carrier of T \ (m `) is set
b is Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
c ` is Element of bool the carrier of T
the carrier of T \ c is set
Cl ft is closed Element of bool the carrier of T
Cl (c `) is closed Element of bool the carrier of T
c is Element of bool the carrier of T
Cl c is closed Element of bool the carrier of T
m is Element of bool the carrier of T
a is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
(T,r) is Element of bool (bool the carrier of T)
[:NAT,(bool the carrier of T):] is non empty set
bool [:NAT,(bool the carrier of T):] is non empty set
m is Element of bool the carrier of T
a is open Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in r . a1 & Cl b1 c= a ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in r . a1 & Cl b1 c= a ) } is set
b is set
r . b is set
{ b1 where b1 is Element of bool the carrier of T : ( b1 in r . b & Cl b1 c= a ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in r . b & Cl b1 c= a ) } is set
ft is set
c is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r . c is set
{ b1 where b1 is Element of bool the carrier of T : ( b1 in r . c & Cl b1 c= a ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in r . c & Cl b1 c= a ) } is set
(T,r,c) is Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : ( b1 in (T,r,c) & Cl b1 c= a ) } is set
R is set
s is Element of bool the carrier of T
Cl s is closed Element of bool the carrier of T
b is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
c is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,r,c) is Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : ( b1 in (T,r,c) & Cl b1 c= a ) } is set
R is set
s is Element of bool the carrier of T
Cl s is closed Element of bool the carrier of T
R is Element of bool (bool the carrier of T)
s is set
B is Element of bool the carrier of T
Cl B is closed Element of bool the carrier of T
union R is Element of bool the carrier of T
Cl () is closed Element of bool the carrier of T
clf R is Element of bool (bool the carrier of T)
union (clf R) is Element of bool the carrier of T
s is set
B is set
U is Element of bool the carrier of T
mfx is Element of bool the carrier of T
Cl mfx is closed Element of bool the carrier of T
x is Element of bool the carrier of T
Cl x is closed Element of bool the carrier of T
the topology of T is non empty open Element of bool (bool the carrier of T)
s is set
B is Element of bool the carrier of T
Cl B is closed Element of bool the carrier of T
b . c is Element of bool the carrier of T
Cl (b . c) is closed Element of bool the carrier of T
Union b is Element of bool the carrier of T
c is set
ft is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . ft is Element of bool the carrier of T
(T,r,ft) is Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : ( b1 in (T,r,ft) & Cl b1 c= a ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in (T,r,ft) & Cl b1 c= a ) } is set
R is