:: 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

[:NAT,REAL:] is non empty V119() V120() V121() set

bool [:NAT,REAL:] is non empty set

bool (bool REAL) 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

[:REAL,REAL:] is non empty V119() V120() V121() set

[:[:REAL,REAL:],REAL:] is non empty V119() V120() V121() set

bool [:[:REAL,REAL:],REAL:] 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 [:REAL,REAL:] 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

RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V213() MetrStruct

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

{} is Function-like functional empty trivial finite V45() countable FinSequence-membered V130() V131() V132() V133() V134() V135() V136() 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

0 is Function-like functional empty trivial ordinal natural V33() real ext-real non positive non negative finite V45() countable FinSequence-membered V63() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT

real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty V14([:REAL,REAL:]) quasi_total V119() V120() V121() Element of bool [:[:REAL,REAL:],REAL:]

MetrStruct(# REAL,real_dist #) is strict MetrStruct

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

TopSpaceMetr RealSpace is TopStruct

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,(Family_open_set RealSpace) #) is non empty strict TopStruct

len omega is cardinal set

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

T is TopSpace-like TopStruct

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

{} T is Function-like functional empty trivial proper finite V45() countable FinSequence-membered open closed compact V130() V131() V132() V133() V134() V135() V136() 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

{..} is non empty trivial finite countable set

{..} is non empty trivial finite countable 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

{..} is non empty trivial finite countable set

{..} is non empty trivial finite countable set

{..} \/ {..} is non empty finite countable 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

{..} is non empty trivial finite countable 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 (union r) 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

{} T is Function-like functional empty trivial proper finite V45() countable FinSequence-membered open closed compact V130() V131() V132() V133() V134() V135() V136() 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 (union r) 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

{ b

c is open Element of bool the carrier of T

{ b

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 countable set

NAT --> {..} is Relation-like NAT -defined {..} -valued Function-like non empty non trivial V14( NAT ) quasi_total non finite Element of bool [:NAT,{..}:]

{..} is non empty trivial finite V45() countable set

[:NAT,{..}:] is non empty set

bool [:NAT,{..}:] 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

{ ([:{b

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 trivial finite countable set

{.{..},.} is non empty finite V45() countable set

{..} is non empty trivial finite countable set

[:{..},T:] is non empty set

[:T,{..}:] is non empty set

[:{..},T:] \/ [:T,{..}:] is non empty set

{..} is non empty trivial finite countable set

[:{..},T:] is non empty set

[:T,{..}:] is non empty set

[:{..},T:] \/ [:T,{..}:] is non empty set

{..} is non empty trivial finite countable set

ft is Element of bool the carrier of (1TopSp [:T,T:])

{ b

{..} \/ {..} is non empty finite countable 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

len T is cardinal set

len a is cardinal set

R is Relation-like Function-like set

dom R is set

s is set

B is set

R . s is set

R . B is set

{..} is non empty trivial finite countable 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

{..} is non empty trivial finite countable 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

s is Relation-like NAT -defined a -valued Function-like quasi_total Element of bool [:NAT,a:]

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 trivial 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 NAT is cardinal set

len (s .: NAT) is cardinal set

a \ (s .: NAT) 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

m is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

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:]

SpaceMetr ( the carrier of T,r) is strict Reflexive discerning symmetric triangle MetrStruct

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

a is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

TopSpaceMetr a is TopStruct

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,(Family_open_set 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 (TopSpaceMetr a) is set

bool the carrier of (TopSpaceMetr a) is non empty set

[#] (TopSpaceMetr a) is non proper Element of bool the carrier of (TopSpaceMetr a)

s is Element of bool the carrier of (TopSpaceMetr a)

([#] (TopSpaceMetr a)) \ s is Element of bool the carrier of (TopSpaceMetr a)

R is Element of the carrier of a

B is Element of bool the carrier of (TopSpaceMetr a)

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 (TopSpaceMetr a)

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 (TopSpaceMetr a) is set

bool the carrier of (TopSpaceMetr a) is non empty set

R is Element of the carrier of (TopSpaceMetr a)

s is Element of the carrier of (TopSpaceMetr a)

B is Element of bool the carrier of (TopSpaceMetr a)

U is Element of bool the carrier of (TopSpaceMetr a)

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:]

SpaceMetr ( the carrier of T,r) is strict Reflexive discerning symmetric triangle MetrStruct

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

a is non empty Reflexive discerning symmetric triangle Discerning MetrStruct

the carrier of a is non empty set

{ (Ball (b

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

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)):]

TopSpaceMetr a is TopStruct

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,(Family_open_set a) #) is non empty strict TopStruct

[#] T is non empty non proper open closed Element of bool the carrier of T

[#] (TopSpaceMetr a) is non proper Element of bool the carrier of (TopSpaceMetr a)

the carrier of (TopSpaceMetr a) is set

bool the carrier of (TopSpaceMetr a) 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 (b

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

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

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

{0} is non empty trivial finite V45() countable V130() V131() V132() V133() V134() V135() Element of bool NAT

{ (Cl (b . b

union { (Cl (b . b

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) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT

{ (Cl (b . b

union { (Cl (b . b

(ft . R) \ (union { (Cl (b . b

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) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT

{ (Cl (b . b

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

{ H

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) \ (union U) 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) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT

{ (Cl (b . b

union { (Cl (b . b

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

R . B is Element of bool the carrier of T

{ (Cl (ft . b

union { (Cl (ft . b

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) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT

{ (Cl (ft . b

union { (Cl (ft . b

(b . s) \ (union { (Cl (ft . b

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) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT

{ (Cl (ft . b

union { (Cl (ft . b

(b . mfx) \ (union { (Cl (ft . b

Seg U is finite U -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT

(Seg U) \/ {0} 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 . b

ft . U is Element of bool the carrier of T

union { (Cl (b . b

(ft . U) \ (union { (Cl (b . b

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) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT

{ (Cl (b . b

union { (Cl (b . b

(ft . U) \ (union { (Cl (b . b

Seg mfx is finite mfx -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT

(Seg mfx) \/ {0} 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 . b

b . mfx is Element of bool the carrier of T

union { (Cl (ft . b

(b . mfx) \ (union { (Cl (ft . b

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) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT

{ (Cl (ft . b

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

{ H

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) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT

{ (Cl (ft . b

union { (Cl (ft . b

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

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

{ b

union { b

b is set

r . b is set

{ b

union { b

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

{ b

union { b

(T,r,c) is Element of bool (bool the carrier of T)

{ b

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)

{ b

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 (union R) 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)

{ b

union { b

R is