:: TOPDIM_1 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool omega is non empty non trivial non finite set

K181() is non empty strict TopSpace-like TopStruct

the carrier of K181() is non empty set

1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

[:1,1:] is non empty Relation-like finite set

bool [:1,1:] is non empty finite V32() set

[:[:1,1:],1:] is non empty Relation-like finite set

bool [:[:1,1:],1:] is non empty finite V32() set

[:[:1,1:],REAL:] is Relation-like set

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

[:REAL,REAL:] is Relation-like set

[:[:REAL,REAL:],REAL:] is Relation-like set

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

2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

[:2,2:] is non empty Relation-like finite set

[:[:2,2:],REAL:] is Relation-like set

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

[:NAT,REAL:] is Relation-like set

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

bool (bool REAL) is non empty set

bool NAT is non empty non trivial non finite set

COMPLEX is set

RAT is set

INT is set

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

K540(2) is V290() L20()

the carrier of K540(2) is set

{} is set

the empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element V89() V90() ext-real non positive non negative integer set is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element V89() V90() ext-real non positive non negative integer set

0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT

union {} is set

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is Element of bool the carrier of TM

Fr Null is closed Element of bool the carrier of TM

Cl Null is closed Element of bool the carrier of TM

Null ` is Element of bool the carrier of TM

the carrier of TM \ Null is set

Cl (Null `) is closed Element of bool the carrier of TM

(Cl Null) /\ (Cl (Null `)) is closed Element of bool the carrier of TM

A is Element of bool the carrier of TM

TM | A is strict TopSpace-like SubSpace of TM

the carrier of (TM | A) is set

bool the carrier of (TM | A) is non empty set

Null /\ A is Element of bool the carrier of TM

(Fr Null) /\ A is Element of bool the carrier of TM

TAN is Element of bool the carrier of (TM | A)

Fr TAN is closed Element of bool the carrier of (TM | A)

Cl TAN is closed Element of bool the carrier of (TM | A)

TAN ` is Element of bool the carrier of (TM | A)

the carrier of (TM | A) \ TAN is set

Cl (TAN `) is closed Element of bool the carrier of (TM | A)

(Cl TAN) /\ (Cl (TAN `)) is closed Element of bool the carrier of (TM | A)

[#] (TM | A) is non proper open closed dense Element of bool the carrier of (TM | A)

[#] TM is non proper open closed dense Element of bool the carrier of TM

N9 is Element of bool the carrier of TM

Cl N9 is closed Element of bool the carrier of TM

(Cl N9) /\ A is Element of bool the carrier of TM

(Cl Null) /\ A is Element of bool the carrier of TM

A \ Null is Element of bool the carrier of TM

A9 is Element of bool the carrier of TM

Cl A9 is closed Element of bool the carrier of TM

(Cl A9) /\ A is Element of bool the carrier of TM

(Cl (Null `)) /\ A is Element of bool the carrier of TM

(Cl A9) /\ ([#] (TM | A)) is Element of bool the carrier of (TM | A)

((Cl Null) /\ A) /\ (Cl (Null `)) is Element of bool the carrier of TM

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is closed Element of bool the carrier of TM

A is closed Element of bool the carrier of TM

TAN is Element of bool the carrier of TM

N9 is Element of bool the carrier of TM

TAN ` is Element of bool the carrier of TM

the carrier of TM \ TAN is set

A9 is Element of bool the carrier of TM

B is Element of bool the carrier of TM

B ` is Element of bool the carrier of TM

the carrier of TM \ B is set

Cl (B `) is closed Element of bool the carrier of TM

N9 ` is Element of bool the carrier of TM

the carrier of TM \ N9 is set

i is Element of bool the carrier of TM

i1 is Element of bool the carrier of TM

b is open Element of bool the carrier of TM

p is open Element of bool the carrier of TM

g is open Element of bool the carrier of TM

i1 ` is Element of bool the carrier of TM

the carrier of TM \ i1 is set

Cl g is closed Element of bool the carrier of TM

Cl (i1 `) is closed Element of bool the carrier of TM

A is open Element of bool the carrier of TM

Cl A is closed Element of bool the carrier of TM

Null is Element of bool the carrier of TM

A is Element of bool the carrier of TM

TAN is open Element of bool the carrier of TM

N9 is open Element of bool the carrier of TM

Cl TAN is closed Element of bool the carrier of TM

Cl N9 is closed Element of bool the carrier of TM

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

{} TM is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer Element of bool the carrier of TM

{({} TM)} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of TM)

TAN is set

N9 is Element of bool (bool the carrier of TM)

A9 is Element of bool the carrier of TM

TM | A9 is strict TopSpace-like SubSpace of TM

the carrier of (TM | A9) is set

bool the carrier of (TM | A9) is non empty set

B is Element of bool the carrier of TM

TM | B is strict TopSpace-like SubSpace of TM

the carrier of (TM | B) is set

bool the carrier of (TM | B) is non empty set

i is Element of the carrier of (TM | B)

i1 is open Element of bool the carrier of (TM | B)

i1 is Element of bool the carrier of TM

TM | i1 is strict TopSpace-like SubSpace of TM

the carrier of (TM | i1) is set

bool the carrier of (TM | i1) is non empty set

B is Element of the carrier of (TM | A9)

i is open Element of bool the carrier of (TM | A9)

b is Element of the carrier of (TM | i1)

p is open Element of bool the carrier of (TM | i1)

[:(bool (bool the carrier of TM)),(bool (bool the carrier of TM)):] is non empty Relation-like set

bool [:(bool (bool the carrier of TM)),(bool (bool the carrier of TM)):] is non empty set

TAN is non empty Relation-like bool (bool the carrier of TM) -defined bool (bool the carrier of TM) -valued Function-like V14( bool (bool the carrier of TM)) quasi_total Element of bool [:(bool (bool the carrier of TM)),(bool (bool the carrier of TM)):]

A is Element of bool (bool the carrier of TM)

N9 is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of TM)):]

N9 . 0 is Element of bool (bool the carrier of TM)

A9 is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of TM)):]

A9 . 0 is Element of bool (bool the carrier of TM)

B is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

B + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

A9 . (B + 1) is Element of bool (bool the carrier of TM)

A9 . B is Element of bool (bool the carrier of TM)

TAN /. (A9 . B) is Element of bool (bool the carrier of TM)

TAN . (A9 . B) is Element of bool (bool the carrier of TM)

TAN . (A9 . B) is Element of bool (bool the carrier of TM)

i is Element of bool the carrier of TM

TM | i is strict TopSpace-like SubSpace of TM

the carrier of (TM | i) is set

bool the carrier of (TM | i) is non empty set

i1 is Element of the carrier of (TM | i)

b is open Element of bool the carrier of (TM | i)

p is Element of bool the carrier of TM

TM | p is strict TopSpace-like SubSpace of TM

the carrier of (TM | p) is set

bool the carrier of (TM | p) is non empty set

B is Element of bool the carrier of TM

TM | B is strict TopSpace-like SubSpace of TM

the carrier of (TM | B) is set

bool the carrier of (TM | B) is non empty set

i is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

A9 . (i + 1) is Element of bool (bool the carrier of TM)

A9 . i is Element of bool (bool the carrier of TM)

i1 is Element of the carrier of (TM | B)

b is open Element of bool the carrier of (TM | B)

p is Element of bool the carrier of TM

A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

A9 . A is Element of bool (bool the carrier of TM)

TM | p is strict TopSpace-like SubSpace of TM

the carrier of (TM | p) is set

bool the carrier of (TM | p) is non empty set

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

A9 . (A + 1) is Element of bool (bool the carrier of TM)

Null is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of TM)):]

Null . 0 is Element of bool (bool the carrier of TM)

A is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of TM)):]

A . 0 is Element of bool (bool the carrier of TM)

TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT

Null . TAN is Element of bool (bool the carrier of TM)

A . TAN is Element of bool (bool the carrier of TM)

TAN + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

Null . (TAN + 1) is Element of bool (bool the carrier of TM)

A . (TAN + 1) is Element of bool (bool the carrier of TM)

N9 is set

A9 is Element of bool the carrier of TM

TM | A9 is strict TopSpace-like SubSpace of TM

the carrier of (TM | A9) is set

bool the carrier of (TM | A9) is non empty set

B is Element of the carrier of (TM | A9)

i is open Element of bool the carrier of (TM | A9)

N9 is set

A9 is Element of bool the carrier of TM

TM | A9 is strict TopSpace-like SubSpace of TM

the carrier of (TM | A9) is set

bool the carrier of (TM | A9) is non empty set

B is Element of the carrier of (TM | A9)

i is open Element of bool the carrier of (TM | A9)

TM is TopSpace-like TopStruct

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of TM)):]

the carrier of TM is set

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

Null is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT

(TM) . Null is Element of bool (bool the carrier of TM)

Null + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

(TM) . (Null + 1) is Element of bool (bool the carrier of TM)

A is set

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

Null is Element of bool the carrier of TM

TM | Null is strict TopSpace-like SubSpace of TM

the carrier of (TM | Null) is set

bool the carrier of (TM | Null) is non empty set

bool the carrier of (TM | Null) is non empty Element of bool (bool the carrier of (TM | Null))

bool (bool the carrier of (TM | Null)) is non empty set

((TM | Null)) is non empty Relation-like NAT -defined bool (bool the carrier of (TM | Null)) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of (TM | Null))):]

bool (bool the carrier of (TM | Null)) is non empty Element of bool (bool (bool the carrier of (TM | Null)))

bool (bool the carrier of (TM | Null)) is non empty set

bool (bool (bool the carrier of (TM | Null))) is non empty set

[:NAT,(bool (bool the carrier of (TM | Null))):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of (TM | Null))):] is non empty non trivial non finite set

A is Element of bool the carrier of TM

TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

((TM | Null)) . TAN is Element of bool (bool the carrier of (TM | Null))

(TM) . TAN is Element of bool (bool the carrier of TM)

A9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

((TM | Null)) . A9 is Element of bool (bool the carrier of (TM | Null))

(TM) . A9 is Element of bool (bool the carrier of TM)

A9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

((TM | Null)) . (A9 + 1) is Element of bool (bool the carrier of (TM | Null))

(TM) . (A9 + 1) is Element of bool (bool the carrier of TM)

i is Element of bool the carrier of (TM | Null)

i1 is Element of bool the carrier of TM

(TM | Null) | i is strict TopSpace-like SubSpace of TM | Null

TM | i1 is strict TopSpace-like SubSpace of TM

[#] (TM | i1) is non proper open closed dense Element of bool the carrier of (TM | i1)

the carrier of (TM | i1) is set

bool the carrier of (TM | i1) is non empty set

[#] TM is non proper open closed dense Element of bool the carrier of TM

the carrier of ((TM | Null) | i) is set

bool the carrier of ((TM | Null) | i) is non empty set

A is Element of the carrier of (TM | i1)

g is open Element of bool the carrier of (TM | i1)

h is open Element of bool the carrier of ((TM | Null) | i)

RngH is open Element of bool the carrier of ((TM | Null) | i)

Fr RngH is closed boundary nowhere_dense Element of bool the carrier of ((TM | Null) | i)

Cl RngH is closed Element of bool the carrier of ((TM | Null) | i)

RngH ` is closed Element of bool the carrier of ((TM | Null) | i)

the carrier of ((TM | Null) | i) \ RngH is set

Cl (RngH `) is closed Element of bool the carrier of ((TM | Null) | i)

(Cl RngH) /\ (Cl (RngH `)) is closed Element of bool the carrier of ((TM | Null) | i)

RngG is open Element of bool the carrier of (TM | i1)

unionG is open Element of bool the carrier of (TM | i1)

Fr unionG is closed boundary nowhere_dense Element of bool the carrier of (TM | i1)

Cl unionG is closed Element of bool the carrier of (TM | i1)

unionG ` is closed Element of bool the carrier of (TM | i1)

the carrier of (TM | i1) \ unionG is set

Cl (unionG `) is closed Element of bool the carrier of (TM | i1)

(Cl unionG) /\ (Cl (unionG `)) is closed Element of bool the carrier of (TM | i1)

the carrier of ((TM | Null) | i) is set

bool the carrier of ((TM | Null) | i) is non empty set

A is Element of the carrier of ((TM | Null) | i)

g is open Element of bool the carrier of ((TM | Null) | i)

[#] ((TM | Null) | i) is non proper open closed dense Element of bool the carrier of ((TM | Null) | i)

the carrier of ((TM | Null) | i) is set

bool the carrier of ((TM | Null) | i) is non empty set

[#] (TM | Null) is non proper open closed dense Element of bool the carrier of (TM | Null)

A is Element of the carrier of ((TM | Null) | i)

g is open Element of bool the carrier of ((TM | Null) | i)

h is open Element of bool the carrier of (TM | i1)

RngH is open Element of bool the carrier of (TM | i1)

Fr RngH is closed boundary nowhere_dense Element of bool the carrier of (TM | i1)

Cl RngH is closed Element of bool the carrier of (TM | i1)

RngH ` is closed Element of bool the carrier of (TM | i1)

the carrier of (TM | i1) \ RngH is set

Cl (RngH `) is closed Element of bool the carrier of (TM | i1)

(Cl RngH) /\ (Cl (RngH `)) is closed Element of bool the carrier of (TM | i1)

RngG is open Element of bool the carrier of ((TM | Null) | i)

unionG is open Element of bool the carrier of ((TM | Null) | i)

Fr unionG is closed boundary nowhere_dense Element of bool the carrier of ((TM | Null) | i)

Cl unionG is closed Element of bool the carrier of ((TM | Null) | i)

unionG ` is closed Element of bool the carrier of ((TM | Null) | i)

the carrier of ((TM | Null) | i) \ unionG is set

Cl (unionG `) is closed Element of bool the carrier of ((TM | Null) | i)

(Cl unionG) /\ (Cl (unionG `)) is closed Element of bool the carrier of ((TM | Null) | i)

A is Element of the carrier of (TM | i1)

g is open Element of bool the carrier of (TM | i1)

((TM | Null)) . 0 is Element of bool (bool the carrier of (TM | Null))

(TM) . 0 is Element of bool (bool the carrier of TM)

{} (TM | Null) is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer Element of bool the carrier of (TM | Null)

{({} (TM | Null))} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of (TM | Null))

{} TM is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer Element of bool the carrier of TM

{({} TM)} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of TM)

N9 is Element of bool the carrier of (TM | Null)

A9 is Element of bool the carrier of TM

N9 is Element of bool the carrier of (TM | Null)

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

Null is Element of bool the carrier of TM

A is Element of bool (bool the carrier of TM)

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

(TM) . TAN is Element of bool (bool the carrier of TM)

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

Null is finite compact Element of bool the carrier of TM

card Null is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of omega

(TM) . (card Null) is Element of bool (bool the carrier of TM)

A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

TAN is TopSpace-like TopStruct

the carrier of TAN is set

bool the carrier of TAN is non empty set

bool the carrier of TAN is non empty Element of bool (bool the carrier of TAN)

bool (bool the carrier of TAN) is non empty set

(TAN) is non empty Relation-like NAT -defined bool (bool the carrier of TAN) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TAN)):]

bool (bool the carrier of TAN) is non empty Element of bool (bool (bool the carrier of TAN))

bool (bool the carrier of TAN) is non empty set

bool (bool (bool the carrier of TAN)) is non empty set

[:NAT,(bool (bool the carrier of TAN)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TAN)):] is non empty non trivial non finite set

N9 is finite compact Element of bool the carrier of TAN

card N9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of omega

(TAN) . (card N9) is Element of bool (bool the carrier of TAN)

TAN | N9 is finite strict TopSpace-like compact SubSpace of TAN

the carrier of (TAN | N9) is finite set

bool the carrier of (TAN | N9) is non empty finite V32() set

(TAN) . A is Element of bool (bool the carrier of TAN)

A9 is Element of the carrier of (TAN | N9)

B is finite open compact Element of bool the carrier of (TAN | N9)

i is finite open compact Element of bool the carrier of (TAN | N9)

Fr i is finite closed boundary nowhere_dense compact Element of bool the carrier of (TAN | N9)

Cl i is finite closed compact Element of bool the carrier of (TAN | N9)

i ` is finite closed compact Element of bool the carrier of (TAN | N9)

the carrier of (TAN | N9) \ i is finite set

Cl (i `) is finite closed compact Element of bool the carrier of (TAN | N9)

(Cl i) /\ (Cl (i `)) is finite closed compact Element of bool the carrier of (TAN | N9)

{A9} is non empty trivial finite 1 -element set

(Cl i) \ i is finite compact Element of bool the carrier of (TAN | N9)

N9 \ i is finite compact Element of bool the carrier of TAN

N9 \ {A9} is finite compact Element of bool the carrier of TAN

[#] (TAN | N9) is non proper finite open closed dense compact Element of bool the carrier of (TAN | N9)

[#] TAN is non proper open closed dense Element of bool the carrier of TAN

card (Fr i) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of omega

card (N9 \ {A9}) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of omega

bool the carrier of (TAN | N9) is non empty finite V32() Element of bool (bool the carrier of (TAN | N9))

bool (bool the carrier of (TAN | N9)) is non empty finite V32() set

((TAN | N9)) is non empty Relation-like NAT -defined bool (bool the carrier of (TAN | N9)) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of (TAN | N9))):]

bool (bool the carrier of (TAN | N9)) is non empty finite V32() Element of bool (bool (bool the carrier of (TAN | N9)))

bool (bool the carrier of (TAN | N9)) is non empty finite V32() set

bool (bool (bool the carrier of (TAN | N9))) is non empty finite V32() set

[:NAT,(bool (bool the carrier of (TAN | N9))):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of (TAN | N9))):] is non empty non trivial non finite set

((TAN | N9)) . (card (Fr i)) is finite V32() Element of bool (bool the carrier of (TAN | N9))

((TAN | N9)) . A is finite V32() Element of bool (bool the carrier of (TAN | N9))

i1 is Element of bool the carrier of TAN

A is TopSpace-like TopStruct

the carrier of A is set

bool the carrier of A is non empty set

bool the carrier of A is non empty Element of bool (bool the carrier of A)

bool (bool the carrier of A) is non empty set

(A) is non empty Relation-like NAT -defined bool (bool the carrier of A) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of A)):]

bool (bool the carrier of A) is non empty Element of bool (bool (bool the carrier of A))

bool (bool the carrier of A) is non empty set

bool (bool (bool the carrier of A)) is non empty set

[:NAT,(bool (bool the carrier of A)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of A)):] is non empty non trivial non finite set

TAN is finite compact Element of bool the carrier of A

card TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of omega

(A) . (card TAN) is Element of bool (bool the carrier of A)

(A) . 0 is Element of bool (bool the carrier of A)

{} A is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer Element of bool the carrier of A

{({} A)} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of A)

A is TopSpace-like TopStruct

the carrier of A is set

bool the carrier of A is non empty set

TAN is finite compact Element of bool the carrier of A

card TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of omega

bool the carrier of A is non empty Element of bool (bool the carrier of A)

bool (bool the carrier of A) is non empty set

(A) is non empty Relation-like NAT -defined bool (bool the carrier of A) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of A)):]

bool (bool the carrier of A) is non empty Element of bool (bool (bool the carrier of A))

bool (bool the carrier of A) is non empty set

bool (bool (bool the carrier of A)) is non empty set

[:NAT,(bool (bool the carrier of A)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of A)):] is non empty non trivial non finite set

(A) . (card TAN) is Element of bool (bool the carrier of A)

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is Element of bool the carrier of TM

bool (bool the carrier of TM) is non empty set

Null is Element of bool (bool the carrier of TM)

{} TM is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer (TM) Element of bool the carrier of TM

{({} TM)} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of TM)

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

(TM) . 0 is Element of bool (bool the carrier of TM)

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

(TM) . 0 is Element of bool (bool the carrier of TM)

{} TM is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer (TM) Element of bool the carrier of TM

{({} TM)} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of TM)

TM is non empty TopSpace-like TopStruct

the carrier of TM is non empty set

bool the carrier of TM is non empty set

[#] TM is non empty non proper open closed dense non boundary Element of bool the carrier of TM

Null is set

{Null} is non empty trivial finite 1 -element set

TM is TopSpace-like TopStruct

[#] TM is non proper open closed dense Element of bool the carrier of TM

the carrier of TM is set

bool the carrier of TM is non empty set

TM is set

1TopSp TM is strict TopSpace-like TopStruct

bool TM is non empty Element of bool (bool TM)

bool TM is non empty set

bool (bool TM) is non empty set

[#] (bool TM) is non empty non proper Element of bool (bool TM)

bool (bool TM) is non empty set

TopStruct(# TM,([#] (bool TM)) #) is strict TopStruct

the carrier of (1TopSp TM) is set

bool the carrier of (1TopSp TM) is non empty Element of bool (bool the carrier of (1TopSp TM))

bool the carrier of (1TopSp TM) is non empty set

bool (bool the carrier of (1TopSp TM)) is non empty set

((1TopSp TM)) is non empty Relation-like NAT -defined bool (bool the carrier of (1TopSp TM)) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of (1TopSp TM))):]

bool (bool the carrier of (1TopSp TM)) is non empty Element of bool (bool (bool the carrier of (1TopSp TM)))

bool (bool the carrier of (1TopSp TM)) is non empty set

bool (bool (bool the carrier of (1TopSp TM))) is non empty set

[:NAT,(bool (bool the carrier of (1TopSp TM))):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of (1TopSp TM))):] is non empty non trivial non finite set

((1TopSp TM)) . 1 is Element of bool (bool the carrier of (1TopSp TM))

[#] (1TopSp TM) is non proper open closed dense Element of bool the carrier of (1TopSp TM)

(1TopSp TM) | ([#] (1TopSp TM)) is strict TopSpace-like SubSpace of 1TopSp TM

the carrier of ((1TopSp TM) | ([#] (1TopSp TM))) is set

bool the carrier of ((1TopSp TM) | ([#] (1TopSp TM))) is non empty set

TAN is Element of the carrier of ((1TopSp TM) | ([#] (1TopSp TM)))

N9 is open Element of bool the carrier of ((1TopSp TM) | ([#] (1TopSp TM)))

[#] ((1TopSp TM) | ([#] (1TopSp TM))) is non proper open closed dense Element of bool the carrier of ((1TopSp TM) | ([#] (1TopSp TM)))

B is Element of bool the carrier of (1TopSp TM)

B ` is Element of bool the carrier of (1TopSp TM)

the carrier of (1TopSp TM) \ B is set

Fr B is closed Element of bool the carrier of (1TopSp TM)

Cl B is closed Element of bool the carrier of (1TopSp TM)

Cl (B `) is closed Element of bool the carrier of (1TopSp TM)

(Cl B) /\ (Cl (B `)) is closed Element of bool the carrier of (1TopSp TM)

{} (1TopSp TM) is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer ( 1TopSp TM) Element of bool the carrier of (1TopSp TM)

(Fr B) /\ ([#] (1TopSp TM)) is closed Element of bool the carrier of (1TopSp TM)

A9 is open Element of bool the carrier of ((1TopSp TM) | ([#] (1TopSp TM)))

A9 /\ ([#] (1TopSp TM)) is Element of bool the carrier of (1TopSp TM)

Fr A9 is closed boundary nowhere_dense Element of bool the carrier of ((1TopSp TM) | ([#] (1TopSp TM)))

Cl A9 is closed Element of bool the carrier of ((1TopSp TM) | ([#] (1TopSp TM)))

A9 ` is closed Element of bool the carrier of ((1TopSp TM) | ([#] (1TopSp TM)))

the carrier of ((1TopSp TM) | ([#] (1TopSp TM))) \ A9 is set

Cl (A9 `) is closed Element of bool the carrier of ((1TopSp TM) | ([#] (1TopSp TM)))

(Cl A9) /\ (Cl (A9 `)) is closed Element of bool the carrier of ((1TopSp TM) | ([#] (1TopSp TM)))

((1TopSp TM)) . 0 is Element of bool (bool the carrier of (1TopSp TM))

{({} (1TopSp TM))} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of (1TopSp TM))

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

((1TopSp TM)) . (0 + 1) is Element of bool (bool the carrier of (1TopSp TM))

TM is set

1TopSp TM is strict TopSpace-like TopStruct

bool TM is non empty Element of bool (bool TM)

bool TM is non empty set

bool (bool TM) is non empty set

[#] (bool TM) is non empty non proper Element of bool (bool TM)

bool (bool TM) is non empty set

TopStruct(# TM,([#] (bool TM)) #) is strict TopStruct

[#] (1TopSp TM) is non proper open closed dense Element of bool the carrier of (1TopSp TM)

the carrier of (1TopSp TM) is set

bool the carrier of (1TopSp TM) is non empty set

bool the carrier of (1TopSp TM) is non empty Element of bool (bool the carrier of (1TopSp TM))

bool (bool the carrier of (1TopSp TM)) is non empty set

((1TopSp TM)) is non empty Relation-like NAT -defined bool (bool the carrier of (1TopSp TM)) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of (1TopSp TM))):]

bool (bool the carrier of (1TopSp TM)) is non empty Element of bool (bool (bool the carrier of (1TopSp TM)))

bool (bool the carrier of (1TopSp TM)) is non empty set

bool (bool (bool the carrier of (1TopSp TM))) is non empty set

[:NAT,(bool (bool the carrier of (1TopSp TM))):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of (1TopSp TM))):] is non empty non trivial non finite set

((1TopSp TM)) . 1 is Element of bool (bool the carrier of (1TopSp TM))

the non empty set is non empty set

1TopSp the non empty set is non empty strict TopSpace-like () TopStruct

bool the non empty set is non empty Element of bool (bool the non empty set )

bool the non empty set is non empty set

bool (bool the non empty set ) is non empty set

[#] (bool the non empty set ) is non empty non proper Element of bool (bool the non empty set )

bool (bool the non empty set ) is non empty set

TopStruct(# the non empty set ,([#] (bool the non empty set )) #) is non empty strict TopStruct

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is Element of bool the carrier of TM

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

(TM) . A is Element of bool (bool the carrier of TM)

A - 1 is V89() V90() ext-real integer Element of REAL

TAN is V89() V90() ext-real integer Element of REAL

TAN + 1 is V89() V90() ext-real integer Element of REAL

(TM) . (TAN + 1) is Element of bool (bool the carrier of TM)

(TM) . TAN is Element of bool (bool the carrier of TM)

dom (TM) is non empty Element of bool NAT

N9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT

N9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

A is V89() V90() ext-real integer set

A + 1 is V89() V90() ext-real integer Element of REAL

(TM) . (A + 1) is Element of bool (bool the carrier of TM)

(TM) . A is Element of bool (bool the carrier of TM)

TAN is V89() V90() ext-real integer set

TAN + 1 is V89() V90() ext-real integer Element of REAL

(TM) . (TAN + 1) is Element of bool (bool the carrier of TM)

(TM) . TAN is Element of bool (bool the carrier of TM)

dom (TM) is non empty Element of bool NAT

A9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT

(TM) . A9 is Element of bool (bool the carrier of TM)

B is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT

(TM) . B is Element of bool (bool the carrier of TM)

N9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT

(TM) . N9 is Element of bool (bool the carrier of TM)

B is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT

(TM) . B is Element of bool (bool the carrier of TM)

- 1 is non empty V89() V90() ext-real non positive negative integer Element of REAL

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is (TM) Element of bool the carrier of TM

(TM,Null) is V89() V90() ext-real integer set

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

1 + (TM,Null) is V89() V90() ext-real integer Element of REAL

(TM) . (1 + (TM,Null)) is Element of bool (bool the carrier of TM)

(TM,Null) + 1 is V89() V90() ext-real integer Element of REAL

dom (TM) is non empty Element of bool NAT

(- 1) + 1 is V89() V90() ext-real integer Element of REAL

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is (TM) Element of bool the carrier of TM

(TM,Null) is V89() V90() ext-real integer set

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

dom (TM) is non empty Element of bool NAT

(TM) . (- 1) is Element of bool (bool the carrier of TM)

(TM) . 0 is Element of bool (bool the carrier of TM)

{} TM is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer (TM) Element of bool the carrier of TM

{({} TM)} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of TM)

(- 1) + 1 is V89() V90() ext-real integer Element of REAL

(TM) . ((- 1) + 1) is Element of bool (bool the carrier of TM)

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is (TM) Element of bool the carrier of TM

(TM,Null) is V89() V90() ext-real integer set

(TM,Null) + 1 is V89() V90() ext-real integer Element of REAL

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

1 + (TM,Null) is V89() V90() ext-real integer Element of REAL

(TM) . (1 + (TM,Null)) is Element of bool (bool the carrier of TM)

dom (TM) is non empty Element of bool NAT

TM is non empty TopSpace-like TopStruct

the carrier of TM is non empty set

bool the carrier of TM is non empty set

Null is non empty (TM) Element of bool the carrier of TM

(TM,Null) is V89() V90() ext-real integer set

(- 1) + 1 is V89() V90() ext-real integer Element of REAL

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

Null is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

Null - 1 is V89() V90() ext-real integer Element of REAL

(TM) . Null is Element of bool (bool the carrier of TM)

A is (TM) Element of bool the carrier of TM

(TM,A) is V89() V90() ext-real integer set

(TM,A) + 1 is V89() V90() ext-real integer Element of REAL

(TM) . ((TM,A) + 1) is Element of bool (bool the carrier of TM)

(Null - 1) + 1 is V89() V90() ext-real integer Element of REAL

(TM) . (TM,A) is Element of bool (bool the carrier of TM)

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is finite compact (TM) Element of bool the carrier of TM

card Null is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of omega

(TM,Null) is V89() V90() ext-real integer set

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

(TM) . (card Null) is Element of bool (bool the carrier of TM)

(card Null) - 1 is V89() V90() ext-real integer Element of REAL

(card Null) - 0 is V89() V90() ext-real integer Element of REAL

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

Null - 1 is V89() V90() ext-real integer Element of REAL

A is (TM) Element of bool the carrier of TM

(TM,A) is V89() V90() ext-real integer set

TM | A is strict TopSpace-like SubSpace of TM

the carrier of (TM | A) is set

bool the carrier of (TM | A) is non empty set

[#] (TM | A) is non proper open closed dense Element of bool the carrier of (TM | A)

[#] TM is non proper open closed dense Element of bool the carrier of TM

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

(TM,A) + 1 is V89() V90() ext-real integer Element of REAL

(TM) . ((TM,A) + 1) is Element of bool (bool the carrier of TM)

(TM) . (TM,A) is Element of bool (bool the carrier of TM)

N9 is Element of the carrier of (TM | A)

A9 is open Element of bool the carrier of (TM | A)

B is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

B - 1 is V89() V90() ext-real integer Element of REAL

(TM) . B is Element of bool (bool the carrier of TM)

i is open Element of bool the carrier of (TM | A)

Fr i is closed boundary nowhere_dense Element of bool the carrier of (TM | A)

Cl i is closed Element of bool the carrier of (TM | A)

i ` is closed Element of bool the carrier of (TM | A)

the carrier of (TM | A) \ i is set

Cl (i `) is closed Element of bool the carrier of (TM | A)

(Cl i) /\ (Cl (i `)) is closed Element of bool the carrier of (TM | A)

i1 is open Element of bool the carrier of (TM | A)

Fr i1 is closed boundary nowhere_dense Element of bool the carrier of (TM | A)

Cl i1 is closed Element of bool the carrier of (TM | A)

i1 ` is closed Element of bool the carrier of (TM | A)

the carrier of (TM | A) \ i1 is set

Cl (i1 `) is closed Element of bool the carrier of (TM | A)

(Cl i1) /\ (Cl (i1 `)) is closed Element of bool the carrier of (TM | A)

bool the carrier of (TM | A) is non empty Element of bool (bool the carrier of (TM | A))

bool (bool the carrier of (TM | A)) is non empty set

((TM | A)) is non empty Relation-like NAT -defined bool (bool the carrier of (TM | A)) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of (TM | A))):]

bool (bool the carrier of (TM | A)) is non empty Element of bool (bool (bool the carrier of (TM | A)))

bool (bool the carrier of (TM | A)) is non empty set

bool (bool (bool the carrier of (TM | A))) is non empty set

[:NAT,(bool (bool the carrier of (TM | A))):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of (TM | A))):] is non empty non trivial non finite set

((TM | A)) . B is Element of bool (bool the carrier of (TM | A))

((TM | A),(Fr i1)) is V89() V90() ext-real integer set

N9 is Element of the carrier of (TM | A)

A9 is open Element of bool the carrier of (TM | A)

B is open Element of bool the carrier of (TM | A)

Fr B is closed boundary nowhere_dense Element of bool the carrier of (TM | A)

Cl B is closed Element of bool the carrier of (TM | A)

B ` is closed Element of bool the carrier of (TM | A)

the carrier of (TM | A) \ B is set

Cl (B `) is closed Element of bool the carrier of (TM | A)

(Cl B) /\ (Cl (B `)) is closed Element of bool the carrier of (TM | A)

((TM | A),(Fr B)) is V89() V90() ext-real integer set

((TM | A)) . Null is Element of bool (bool the carrier of (TM | A))

(TM) . Null is Element of bool (bool the carrier of TM)

Null + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

(TM) . (Null + 1) is Element of bool (bool the carrier of TM)

(Null + 1) - 1 is V89() V90() ext-real integer Element of REAL

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

Null is Element of bool (bool the carrier of TM)

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

(TM) . A is Element of bool (bool the carrier of TM)

A - 1 is V89() V90() ext-real integer Element of REAL

TAN is V89() V90() ext-real integer Element of REAL

TAN + 1 is V89() V90() ext-real integer Element of REAL

(TM) . (TAN + 1) is Element of bool (bool the carrier of TM)

N9 is V89() V90() ext-real integer set

N9 + 1 is V89() V90() ext-real integer Element of REAL

(TM) . (N9 + 1) is Element of bool (bool the carrier of TM)

(- 1) + 1 is V89() V90() ext-real integer Element of REAL

TAN + 1 is V89() V90() ext-real integer Element of REAL

A9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

0 - 1 is V89() V90() ext-real integer Element of REAL

N9 is V89() V90() ext-real integer set

N9 + 1 is V89() V90() ext-real integer Element of REAL

(TM) . (N9 + 1) is Element of bool (bool the carrier of TM)

A is V89() V90() ext-real integer set

A + 1 is V89() V90() ext-real integer Element of REAL

(TM) . (A + 1) is Element of bool (bool the carrier of TM)

TAN is V89() V90() ext-real integer set

TAN + 1 is V89() V90() ext-real integer Element of REAL

(TM) . (TAN + 1) is Element of bool (bool the carrier of TM)

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

{} TM is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer (TM) Element of bool the carrier of TM

{({} TM)} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of TM)

Null is Element of bool (bool the carrier of TM)

(TM,Null) is V89() V90() ext-real integer set

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

(TM) . 0 is Element of bool (bool the carrier of TM)

(- 1) + 1 is V89() V90() ext-real integer Element of REAL

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

Null is Element of bool (bool the carrier of TM)

(TM,Null) is V89() V90() ext-real integer set

A is V89() V90() ext-real integer set

(- 1) + 1 is V89() V90() ext-real integer Element of REAL

(TM,Null) + 1 is V89() V90() ext-real integer Element of REAL

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

(TM) . TAN is Element of bool (bool the carrier of TM)

N9 is Element of bool the carrier of TM

(TM,N9) is V89() V90() ext-real integer set

TAN - 1 is V89() V90() ext-real integer Element of REAL

A + 1 is V89() V90() ext-real integer Element of REAL

TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT

(TM) . TAN is Element of bool (bool the carrier of TM)

N9 is set

TAN - 1 is V89() V90() ext-real integer Element of REAL

A9 is Element of bool the carrier of TM

(TM,A9) is V89() V90() ext-real integer set

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

Null is Element of bool (bool the carrier of TM)

(TM,Null) is V89() V90() ext-real integer set

A is Element of bool (bool the carrier of TM)

(TM,A) is V89() V90() ext-real integer set

TAN is Element of bool the carrier of TM

(TM,TAN) is V89() V90() ext-real integer set

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

Null is Element of bool (bool the carrier of TM)

(TM,Null) is V89() V90() ext-real integer set

A is Element of bool (bool the carrier of TM)

(TM,A) is V89() V90() ext-real integer set

Null \/ A is Element of bool (bool the carrier of TM)

(TM,(Null \/ A)) is V89() V90() ext-real integer set

TAN is V89() V90() ext-real integer set

N9 is Element of bool the carrier of TM

(TM,N9) is V89() V90() ext-real integer set

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

Null is (TM) Element of bool (bool the carrier of TM)

A is (TM) Element of bool (bool the carrier of TM)

Null \/ A is Element of bool (bool the carrier of TM)

(TM,Null) is V89() V90() ext-real integer set

(TM,Null) + 1 is V89() V90() ext-real integer Element of REAL

(TM,A) is V89() V90() ext-real integer set

(TM,A) + 1 is V89() V90() ext-real integer Element of REAL

(- 1) + 1 is V89() V90() ext-real integer Element of REAL

(TM,Null) + 0 is V89() V90() ext-real integer Element of REAL

((TM,Null) + 1) + ((TM,A) + 1) is V89() V90() ext-real integer Element of REAL

(TM,A) + 0 is V89() V90() ext-real integer Element of REAL

((TM,A) + 1) + ((TM,Null) + 1) is V89() V90() ext-real integer Element of REAL

A9 is Element of bool (bool the carrier of TM)

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

bool (bool the carrier of TM) is non empty set

Null is Element of bool (bool the carrier of TM)

A is Element of bool (bool the carrier of TM)

(TM,Null) is V89() V90() ext-real integer set

TAN is V89() V90() ext-real integer set

(TM,A) is V89() V90() ext-real integer set

Null \/ A is Element of bool (bool the carrier of TM)

(TM,(Null \/ A)) is V89() V90() ext-real integer set

TM is TopSpace-like TopStruct

[#] TM is non proper open closed dense Element of bool the carrier of TM

the carrier of TM is set

bool the carrier of TM is non empty set

(TM,([#] TM)) is V89() V90() ext-real integer set

TM is non empty TopSpace-like () TopStruct

(TM) is V89() V90() ext-real integer set

[#] TM is non empty non proper open closed dense non boundary Element of bool the carrier of TM

the carrier of TM is non empty set

bool the carrier of TM is non empty set

(TM,([#] TM)) is V89() V90() ext-real integer set

TM is non empty set

1TopSp TM is non empty strict TopSpace-like () TopStruct

bool TM is non empty Element of bool (bool TM)

bool TM is non empty set

bool (bool TM) is non empty set

[#] (bool TM) is non empty non proper Element of bool (bool TM)

bool (bool TM) is non empty set

TopStruct(# TM,([#] (bool TM)) #) is non empty strict TopStruct

((1TopSp TM)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

[#] (1TopSp TM) is non empty non proper open closed dense non boundary Element of bool the carrier of (1TopSp TM)

the carrier of (1TopSp TM) is non empty set

bool the carrier of (1TopSp TM) is non empty set

((1TopSp TM),([#] (1TopSp TM))) is V89() V90() ext-real integer set

bool the carrier of (1TopSp TM) is non empty Element of bool (bool the carrier of (1TopSp TM))

bool (bool the carrier of (1TopSp TM)) is non empty set

((1TopSp TM)) is non empty Relation-like NAT -defined bool (bool the carrier of (1TopSp TM)) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of (1TopSp TM))):]

bool (bool the carrier of (1TopSp TM)) is non empty Element of bool (bool (bool the carrier of (1TopSp TM)))

bool (bool the carrier of (1TopSp TM)) is non empty set

bool (bool (bool the carrier of (1TopSp TM))) is non empty set

[:NAT,(bool (bool the carrier of (1TopSp TM))):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of (1TopSp TM))):] is non empty non trivial non finite set

((1TopSp TM)) . 0 is Element of bool (bool the carrier of (1TopSp TM))

{} (1TopSp TM) is empty proper Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element open closed boundary nowhere_dense V89() V90() compact ext-real non positive non negative integer ( 1TopSp TM) Element of bool the carrier of (1TopSp TM)

{({} (1TopSp TM))} is non empty trivial finite V32() 1 -element Element of bool (bool the carrier of (1TopSp TM))

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

((1TopSp TM)) . (0 + 1) is Element of bool (bool the carrier of (1TopSp TM))

TM is TopSpace-like TopStruct

the carrier of TM is set

bool the carrier of TM is non empty set

Null is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

Null - 1 is V89() V90() ext-real integer Element of REAL

[#] TM is non proper open closed dense Element of bool the carrier of TM

TM | ([#] TM) is strict TopSpace-like SubSpace of TM

[#] (TM | ([#] TM)) is non proper open closed dense Element of bool the carrier of (TM | ([#] TM))

the carrier of (TM | ([#] TM)) is set

bool the carrier of (TM | ([#] TM)) is non empty set

the topology of TM is non empty open Element of bool (bool the carrier of TM)

bool (bool the carrier of TM) is non empty set

TopStruct(# the carrier of TM, the topology of TM #) is strict TopSpace-like TopStruct

the topology of (TM | ([#] TM)) is non empty open Element of bool (bool the carrier of (TM | ([#] TM)))

bool (bool the carrier of (TM | ([#] TM))) is non empty set

TopStruct(# the carrier of (TM | ([#] TM)), the topology of (TM | ([#] TM)) #) is strict TopSpace-like TopStruct

N9 is Element of the carrier of (TM | ([#] TM))

A9 is open Element of bool the carrier of (TM | ([#] TM))

B is Element of the carrier of TM

i is open Element of bool the carrier of TM

i1 is open Element of bool the carrier of TM

Fr i1 is closed boundary nowhere_dense Element of bool the carrier of TM

Cl i1 is closed Element of bool the carrier of TM

i1 ` is closed Element of bool the carrier of TM

the carrier of TM \ i1 is set

Cl (i1 `) is closed Element of bool the carrier of TM

(Cl i1) /\ (Cl (i1 `)) is closed Element of bool the carrier of TM

(TM,(Fr i1)) is V89() V90() ext-real integer set

b is open Element of bool the carrier of (TM | ([#] TM))

p is open Element of bool the carrier of (TM | ([#] TM))

Cl p is closed Element of bool the carrier of (TM | ([#] TM))

Int i1 is open Element of bool the carrier of TM

(Cl (i1 `)) ` is open Element of bool the carrier of TM

the carrier of TM \ (Cl (i1 `)) is set

Int p is open Element of bool the carrier of (TM | ([#] TM))

p ` is closed Element of bool the carrier of (TM | ([#] TM))

the carrier of (TM | ([#] TM)) \ p is set

Cl (p `) is closed Element of bool the carrier of (TM | ([#] TM))

(Cl (p `)) ` is open Element of bool the carrier of (TM | ([#] TM))

the carrier of (TM | ([#] TM)) \ (Cl (p `)) is set

(Cl p) \ (Int p) is Element of bool the carrier of (TM | ([#] TM))

Fr p is closed boundary nowhere_dense Element of bool the carrier of (TM | ([#] TM))

(Cl p) /\ (Cl (p `)) is closed Element of bool the carrier of (TM | ([#] TM))

bool the carrier of TM is non empty Element of bool (bool the carrier of TM)

(TM) is non empty Relation-like NAT -defined bool (bool the carrier of TM) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of TM)):]

bool (bool the carrier of TM) is non empty Element of bool (bool (bool the carrier of TM))

bool (bool the carrier of TM) is non empty set

bool (bool (bool the carrier of TM)) is non empty set

[:NAT,(bool (bool the carrier of TM)):] is non empty non trivial Relation-like non finite set

bool [:NAT,(bool (bool the carrier of TM)):] is non empty non trivial non finite set

(TM) . Null is Element of bool (bool the carrier of TM)

Null + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT

(TM) . (Null + 1) is Element of bool (bool the carrier of TM)

TM is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set

TM - 1 is V89() V90() ext-re