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