:: 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-real integer Element of REAL
Null is TopSpace-like () TopStruct
(Null) is V89() V90() ext-real integer set
[#] Null is non proper open closed dense Element of bool the carrier of Null
the carrier of Null is set
bool the carrier of Null is non empty set
(Null,([#] Null)) is V89() V90() ext-real integer set
Null | ([#] Null) is strict TopSpace-like SubSpace of Null
[#] (Null | ([#] Null)) is non proper open closed dense Element of bool the carrier of (Null | ([#] Null))
the carrier of (Null | ([#] Null)) is set
bool the carrier of (Null | ([#] Null)) is non empty set
the topology of Null is non empty open Element of bool (bool the carrier of Null)
bool (bool the carrier of Null) is non empty set
TopStruct(# the carrier of Null, the topology of Null #) is strict TopSpace-like TopStruct
the topology of (Null | ([#] Null)) is non empty open Element of bool (bool the carrier of (Null | ([#] Null)))
bool (bool the carrier of (Null | ([#] Null))) is non empty set
TopStruct(# the carrier of (Null | ([#] Null)), the topology of (Null | ([#] Null)) #) is strict TopSpace-like TopStruct
N9 is Element of the carrier of Null
A9 is open Element of bool the carrier of Null
B is Element of the carrier of (Null | ([#] Null))
i is open Element of bool the carrier of (Null | ([#] Null))
i1 is open Element of bool the carrier of (Null | ([#] Null))
Fr i1 is closed boundary nowhere_dense Element of bool the carrier of (Null | ([#] Null))
Cl i1 is closed Element of bool the carrier of (Null | ([#] Null))
i1 ` is closed Element of bool the carrier of (Null | ([#] Null))
the carrier of (Null | ([#] Null)) \ i1 is set
Cl (i1 `) is closed Element of bool the carrier of (Null | ([#] Null))
(Cl i1) /\ (Cl (i1 `)) is closed Element of bool the carrier of (Null | ([#] Null))
((Null | ([#] Null)),(Fr i1)) is V89() V90() ext-real integer set
b is open Element of bool the carrier of Null
Cl b is closed Element of bool the carrier of Null
Int b is open Element of bool the carrier of Null
b ` is closed Element of bool the carrier of Null
the carrier of Null \ b is set
Cl (b `) is closed Element of bool the carrier of Null
(Cl (b `)) ` is open Element of bool the carrier of Null
the carrier of Null \ (Cl (b `)) is set
Int i1 is open Element of bool the carrier of (Null | ([#] Null))
(Cl (i1 `)) ` is open Element of bool the carrier of (Null | ([#] Null))
the carrier of (Null | ([#] Null)) \ (Cl (i1 `)) is set
Fr b is closed boundary nowhere_dense Element of bool the carrier of Null
(Cl b) /\ (Cl (b `)) is closed Element of bool the carrier of Null
(Cl i1) \ (Int i1) is Element of bool the carrier of (Null | ([#] Null))
bool the carrier of (Null | ([#] Null)) is non empty Element of bool (bool the carrier of (Null | ([#] Null)))
((Null | ([#] Null))) is non empty Relation-like NAT -defined bool (bool the carrier of (Null | ([#] Null))) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of (Null | ([#] Null)))):]
bool (bool the carrier of (Null | ([#] Null))) is non empty Element of bool (bool (bool the carrier of (Null | ([#] Null))))
bool (bool the carrier of (Null | ([#] Null))) is non empty set
bool (bool (bool the carrier of (Null | ([#] Null)))) is non empty set
[:NAT,(bool (bool the carrier of (Null | ([#] Null)))):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (bool the carrier of (Null | ([#] Null)))):] is non empty non trivial non finite set
((Null | ([#] Null))) . TM is Element of bool (bool the carrier of (Null | ([#] Null)))
p is open Element of bool the carrier of Null
Fr p is closed boundary nowhere_dense Element of bool the carrier of Null
Cl p is closed Element of bool the carrier of Null
p ` is closed Element of bool the carrier of Null
the carrier of Null \ p is set
Cl (p `) is closed Element of bool the carrier of Null
(Cl p) /\ (Cl (p `)) is closed Element of bool the carrier of Null
bool the carrier of Null is non empty Element of bool (bool the carrier of Null)
(Null) is non empty Relation-like NAT -defined bool (bool the carrier of Null) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of Null)):]
bool (bool the carrier of Null) is non empty Element of bool (bool (bool the carrier of Null))
bool (bool the carrier of Null) is non empty set
bool (bool (bool the carrier of Null)) is non empty set
[:NAT,(bool (bool the carrier of Null)):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (bool the carrier of Null)):] is non empty non trivial non finite set
(Null) . TM is Element of bool (bool the carrier of Null)
(Null,(Fr p)) is V89() V90() ext-real integer set
N9 is Element of the carrier of (Null | ([#] Null))
A9 is open Element of bool the carrier of (Null | ([#] Null))
B is Element of the carrier of Null
i is open Element of bool the carrier of Null
i1 is open Element of bool the carrier of Null
Fr i1 is closed boundary nowhere_dense Element of bool the carrier of Null
Cl i1 is closed Element of bool the carrier of Null
i1 ` is closed Element of bool the carrier of Null
the carrier of Null \ i1 is set
Cl (i1 `) is closed Element of bool the carrier of Null
(Cl i1) /\ (Cl (i1 `)) is closed Element of bool the carrier of Null
(Null,(Fr i1)) is V89() V90() ext-real integer set
b is open Element of bool the carrier of (Null | ([#] Null))
Cl b is closed Element of bool the carrier of (Null | ([#] Null))
Int i1 is open Element of bool the carrier of Null
(Cl (i1 `)) ` is open Element of bool the carrier of Null
the carrier of Null \ (Cl (i1 `)) is set
Int b is open Element of bool the carrier of (Null | ([#] Null))
b ` is closed Element of bool the carrier of (Null | ([#] Null))
the carrier of (Null | ([#] Null)) \ b is set
Cl (b `) is closed Element of bool the carrier of (Null | ([#] Null))
(Cl (b `)) ` is open Element of bool the carrier of (Null | ([#] Null))
the carrier of (Null | ([#] Null)) \ (Cl (b `)) is set
(Cl b) \ (Int b) is Element of bool the carrier of (Null | ([#] Null))
Fr b is closed boundary nowhere_dense Element of bool the carrier of (Null | ([#] Null))
(Cl b) /\ (Cl (b `)) is closed Element of bool the carrier of (Null | ([#] Null))
p is open Element of bool the carrier of (Null | ([#] Null))
Fr p is closed boundary nowhere_dense Element of bool the carrier of (Null | ([#] Null))
Cl p is closed Element of bool the carrier of (Null | ([#] Null))
p ` is closed Element of bool the carrier of (Null | ([#] Null))
the carrier of (Null | ([#] Null)) \ p is set
Cl (p `) is closed Element of bool the carrier of (Null | ([#] Null))
(Cl p) /\ (Cl (p `)) is closed Element of bool the carrier of (Null | ([#] Null))
((Null | ([#] Null)),(Fr p)) 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
Null is (TM) Element of bool the carrier of TM
TM | Null is strict TopSpace-like SubSpace of TM
((TM | Null)) is V89() V90() ext-real integer set
[#] (TM | Null) is non proper open closed dense Element of bool the carrier of (TM | Null)
the carrier of (TM | Null) is set
bool the carrier of (TM | Null) is non empty set
((TM | Null),([#] (TM | Null))) is V89() V90() ext-real integer set
(TM,Null) is V89() V90() ext-real integer 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
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
TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
TAN + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT
(TM) . (TAN + 1) is Element of bool (bool the carrier of TM)
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
((TM | Null)) . (TAN + 1) is Element of bool (bool the carrier of (TM | Null))
((TM | Null),([#] (TM | Null))) + 1 is V89() V90() ext-real integer Element of REAL
(((TM | Null),([#] (TM | Null))) + 1) - 1 is V89() V90() ext-real integer Element of REAL
TAN - 1 is V89() V90() ext-real integer Element of REAL
((TM | Null)) . TAN is Element of bool (bool the carrier of (TM | Null))
(TM) . TAN is Element of bool (bool the carrier of TM)
(TAN + 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
(TM) is V89() V90() ext-real integer set
[#] TM is non proper open closed dense Element of bool the carrier of TM
(TM,([#] TM)) is V89() V90() ext-real integer set
(TM) + 1 is V89() V90() ext-real integer Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
A - 1 is V89() V90() ext-real integer Element of REAL
TAN is TopSpace-like TopStruct
(TAN) is V89() V90() ext-real integer set
[#] TAN is non proper open closed dense Element of bool the carrier of TAN
the carrier of TAN is set
bool the carrier of TAN is non empty set
(TAN,([#] TAN)) is V89() V90() ext-real integer set
N9 is Element of bool the carrier of TAN
TAN | N9 is strict TopSpace-like SubSpace of TAN
((TAN | N9)) is V89() V90() ext-real integer set
[#] (TAN | N9) is non proper open closed dense Element of bool the carrier of (TAN | N9)
the carrier of (TAN | N9) is set
bool the carrier of (TAN | N9) is non empty set
((TAN | N9),([#] (TAN | N9))) is V89() V90() ext-real integer set
{} TAN 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 (TAN) Element of bool the carrier of TAN
N9 is TopSpace-like TopStruct
(N9) is V89() V90() ext-real integer set
[#] N9 is non proper open closed dense Element of bool the carrier of N9
the carrier of N9 is set
bool the carrier of N9 is non empty set
(N9,([#] N9)) is V89() V90() ext-real integer set
A9 is Element of bool the carrier of N9
N9 | A9 is strict TopSpace-like SubSpace of N9
((N9 | A9)) is V89() V90() ext-real integer set
[#] (N9 | A9) is non proper open closed dense Element of bool the carrier of (N9 | A9)
the carrier of (N9 | A9) is set
bool the carrier of (N9 | A9) is non empty set
((N9 | A9),([#] (N9 | A9))) is V89() V90() ext-real integer set
i is Element of the carrier of (N9 | A9)
i1 is open Element of bool the carrier of (N9 | A9)
the topology of (N9 | A9) is non empty open Element of bool (bool the carrier of (N9 | A9))
bool (bool the carrier of (N9 | A9)) is non empty set
the topology of N9 is non empty open Element of bool (bool the carrier of N9)
bool (bool the carrier of N9) is non empty set
b is Element of bool the carrier of N9
b /\ ([#] (N9 | A9)) is Element of bool the carrier of (N9 | A9)
p is Element of the carrier of N9
TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
TAN - 1 is V89() V90() ext-real integer Element of REAL
A is open Element of bool the carrier of N9
Fr A is closed boundary nowhere_dense Element of bool the carrier of N9
Cl A is closed Element of bool the carrier of N9
A ` is closed Element of bool the carrier of N9
the carrier of N9 \ A is set
Cl (A `) is closed Element of bool the carrier of N9
(Cl A) /\ (Cl (A `)) is closed Element of bool the carrier of N9
(N9,(Fr A)) is V89() V90() ext-real integer set
(N9,(Fr A)) + 1 is V89() V90() ext-real integer Element of REAL
((N9,(Fr A)) + 1) - 1 is V89() V90() ext-real integer Element of REAL
A - 0 is V89() V90() ext-real integer Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
g - 1 is V89() V90() ext-real integer Element of REAL
h is TopSpace-like TopStruct
the carrier of h is set
bool the carrier of h is non empty set
(h) is V89() V90() ext-real integer set
[#] h is non proper open closed dense Element of bool the carrier of h
(h,([#] h)) is V89() V90() ext-real integer set
RngH is Element of bool the carrier of h
h | RngH is strict TopSpace-like SubSpace of h
RngG is Element of bool the carrier of h
h | RngG is strict TopSpace-like SubSpace of h
((h | RngG)) is V89() V90() ext-real integer set
[#] (h | RngG) is non proper open closed dense Element of bool the carrier of (h | RngG)
the carrier of (h | RngG) is set
bool the carrier of (h | RngG) is non empty set
((h | RngG),([#] (h | RngG))) is V89() V90() ext-real integer set
A /\ ([#] (N9 | A9)) is Element of bool the carrier of (N9 | A9)
h is Element of bool the carrier of (N9 | A9)
N9 | (Fr A) is strict TopSpace-like SubSpace of N9
[#] (N9 | (Fr A)) is non proper open closed dense Element of bool the carrier of (N9 | (Fr A))
the carrier of (N9 | (Fr A)) is set
bool the carrier of (N9 | (Fr A)) is non empty set
RngH is open Element of bool the carrier of (N9 | A9)
Fr RngH is closed boundary nowhere_dense Element of bool the carrier of (N9 | A9)
Cl RngH is closed Element of bool the carrier of (N9 | A9)
RngH ` is closed Element of bool the carrier of (N9 | A9)
the carrier of (N9 | A9) \ RngH is set
Cl (RngH `) is closed Element of bool the carrier of (N9 | A9)
(Cl RngH) /\ (Cl (RngH `)) is closed Element of bool the carrier of (N9 | A9)
(Fr A) /\ A9 is Element of bool the carrier of N9
unionH is Element of bool the carrier of (N9 | (Fr A))
((N9 | (Fr A))) is V89() V90() ext-real integer set
((N9 | (Fr A)),([#] (N9 | (Fr A)))) is V89() V90() ext-real integer set
(N9 | (Fr A)) | unionH is strict TopSpace-like SubSpace of N9 | (Fr A)
[#] ((N9 | (Fr A)) | unionH) is non proper open closed dense Element of bool the carrier of ((N9 | (Fr A)) | unionH)
the carrier of ((N9 | (Fr A)) | unionH) is set
bool the carrier of ((N9 | (Fr A)) | unionH) is non empty set
(((N9 | (Fr A)) | unionH)) is V89() V90() ext-real integer set
(((N9 | (Fr A)) | unionH),([#] ((N9 | (Fr A)) | unionH))) is V89() V90() ext-real integer set
bool the carrier of ((N9 | (Fr A)) | unionH) is non empty Element of bool (bool the carrier of ((N9 | (Fr A)) | unionH))
bool (bool the carrier of ((N9 | (Fr A)) | unionH)) is non empty set
(((N9 | (Fr A)) | unionH)) is non empty Relation-like NAT -defined bool (bool the carrier of ((N9 | (Fr A)) | unionH)) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of ((N9 | (Fr A)) | unionH))):]
bool (bool the carrier of ((N9 | (Fr A)) | unionH)) is non empty Element of bool (bool (bool the carrier of ((N9 | (Fr A)) | unionH)))
bool (bool the carrier of ((N9 | (Fr A)) | unionH)) is non empty set
bool (bool (bool the carrier of ((N9 | (Fr A)) | unionH))) is non empty set
[:NAT,(bool (bool the carrier of ((N9 | (Fr A)) | unionH))):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (bool the carrier of ((N9 | (Fr A)) | unionH))):] is non empty non trivial non finite set
(((N9 | (Fr A)) | unionH)) . TAN is Element of bool (bool the carrier of ((N9 | (Fr A)) | unionH))
bool the carrier of (N9 | (Fr A)) is non empty Element of bool (bool the carrier of (N9 | (Fr A)))
bool (bool the carrier of (N9 | (Fr A))) is non empty set
((N9 | (Fr A))) is non empty Relation-like NAT -defined bool (bool the carrier of (N9 | (Fr A))) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of (N9 | (Fr A)))):]
bool (bool the carrier of (N9 | (Fr A))) is non empty Element of bool (bool (bool the carrier of (N9 | (Fr A))))
bool (bool the carrier of (N9 | (Fr A))) is non empty set
bool (bool (bool the carrier of (N9 | (Fr A)))) is non empty set
[:NAT,(bool (bool the carrier of (N9 | (Fr A)))):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (bool the carrier of (N9 | (Fr A)))):] is non empty non trivial non finite set
((N9 | (Fr A))) . TAN is Element of bool (bool the carrier of (N9 | (Fr A)))
unionH is Element of bool the carrier of N9
bool the carrier of N9 is non empty Element of bool (bool the carrier of N9)
(N9) is non empty Relation-like NAT -defined bool (bool the carrier of N9) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of N9)):]
bool (bool the carrier of N9) is non empty Element of bool (bool (bool the carrier of N9))
bool (bool the carrier of N9) is non empty set
bool (bool (bool the carrier of N9)) is non empty set
[:NAT,(bool (bool the carrier of N9)):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (bool the carrier of N9)):] is non empty non trivial non finite set
(N9) . TAN is Element of bool (bool the carrier of N9)
unionG is open Element of bool the carrier of (N9 | A9)
Fr unionG is closed boundary nowhere_dense Element of bool the carrier of (N9 | A9)
Cl unionG is closed Element of bool the carrier of (N9 | A9)
unionG ` is closed Element of bool the carrier of (N9 | A9)
the carrier of (N9 | A9) \ unionG is set
Cl (unionG `) is closed Element of bool the carrier of (N9 | A9)
(Cl unionG) /\ (Cl (unionG `)) is closed Element of bool the carrier of (N9 | A9)
bool the carrier of (N9 | A9) is non empty Element of bool (bool the carrier of (N9 | A9))
((N9 | A9)) is non empty Relation-like NAT -defined bool (bool the carrier of (N9 | A9)) -valued Function-like V14( NAT ) quasi_total non-descending Element of bool [:NAT,(bool (bool the carrier of (N9 | A9))):]
bool (bool the carrier of (N9 | A9)) is non empty Element of bool (bool (bool the carrier of (N9 | A9)))
bool (bool the carrier of (N9 | A9)) is non empty set
bool (bool (bool the carrier of (N9 | A9))) is non empty set
[:NAT,(bool (bool the carrier of (N9 | A9))):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool (bool the carrier of (N9 | A9))):] is non empty non trivial non finite set
((N9 | A9)) . TAN is Element of bool (bool the carrier of (N9 | A9))
((N9 | A9),(Fr unionG)) is V89() V90() ext-real integer 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 TopSpace-like TopStruct
the carrier of A is set
bool the carrier of A is non empty set
(A) is V89() V90() ext-real integer set
[#] A is non proper open closed dense Element of bool the carrier of A
(A,([#] A)) is V89() V90() ext-real integer set
TAN is Element of bool the carrier of A
A | TAN is strict TopSpace-like SubSpace of A
N9 is Element of bool the carrier of A
A | N9 is strict TopSpace-like SubSpace of A
((A | N9)) is V89() V90() ext-real integer set
[#] (A | N9) is non proper open closed dense Element of bool the carrier of (A | N9)
the carrier of (A | N9) is set
bool the carrier of (A | N9) is non empty set
((A | N9),([#] (A | N9))) is V89() V90() ext-real integer set
A is Element of bool the carrier of TM
TM | A is strict TopSpace-like SubSpace of TM
TAN is Element of bool the carrier of TM
TM | TAN is strict TopSpace-like SubSpace of TM
((TM | TAN)) is V89() V90() ext-real integer set
[#] (TM | TAN) is non proper open closed dense Element of bool the carrier of (TM | TAN)
the carrier of (TM | TAN) is set
bool the carrier of (TM | TAN) is non empty set
((TM | TAN),([#] (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
Null is Element of bool the carrier of TM
TM | Null is strict TopSpace-like SubSpace of TM
[#] (TM | Null) is non proper open closed dense Element of bool the carrier of (TM | Null)
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
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))
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) . 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
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 (TM) Element of bool the carrier of TM
TM | Null is strict TopSpace-like SubSpace 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 strict TopSpace-like () SubSpace of TM
((TM | Null)) is V89() V90() ext-real integer set
[#] (TM | Null) is non proper open closed dense (TM | Null) Element of bool the carrier of (TM | Null)
the carrier of (TM | Null) is set
bool the carrier of (TM | Null) is non empty set
((TM | Null),([#] (TM | Null))) is V89() V90() ext-real integer set
(TM,Null) 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
Null is Element of bool the carrier of TM
TM | Null is strict TopSpace-like SubSpace of TM
[#] (TM | Null) is non proper open closed dense Element of bool the carrier of (TM | Null)
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 epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
((TM | Null)) . A is Element of bool (bool the carrier of (TM | Null))
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 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 Element of bool the carrier of TM
(TM,Null) is V89() V90() ext-real integer set
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
[#] (TM | A) is non proper open closed dense (TM | A) Element of bool the carrier of (TM | A)
the carrier of (TM | A) is set
bool the carrier of (TM | A) is non empty set
((TM | A)) is V89() V90() ext-real integer set
((TM | A),([#] (TM | A))) is V89() V90() ext-real integer set
TAN is (TM | A) Element of bool the carrier of (TM | A)
(TM | A) | TAN is strict TopSpace-like () SubSpace of TM | A
TM | Null is strict TopSpace-like SubSpace of TM
((TM | Null)) is V89() V90() ext-real integer set
[#] (TM | Null) is non proper open closed dense Element of bool the carrier of (TM | Null)
the carrier of (TM | Null) is set
bool the carrier of (TM | Null) is non empty set
((TM | Null),([#] (TM | Null))) 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
Null is (TM) Element of bool the carrier of TM
(TM,Null) is V89() V90() ext-real integer set
(TM) is V89() V90() ext-real integer set
[#] TM is non proper open closed dense (TM) Element of bool the carrier of TM
(TM,([#] TM)) 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
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
A is Element of bool the carrier of TM
(TM,A) is V89() V90() ext-real integer set
TAN is Element of bool the carrier of (TM | Null)
((TM | Null),TAN) is V89() V90() ext-real integer set
(TM | Null) | TAN is strict TopSpace-like SubSpace of TM | Null
TM | A is strict TopSpace-like SubSpace of TM
(((TM | Null) | TAN)) is V89() V90() ext-real integer set
[#] ((TM | Null) | TAN) is non proper open closed dense Element of bool the carrier of ((TM | Null) | TAN)
the carrier of ((TM | Null) | TAN) is set
bool the carrier of ((TM | Null) | TAN) is non empty set
(((TM | Null) | TAN),([#] ((TM | Null) | TAN))) is V89() V90() ext-real integer set
((TM | A)) is V89() V90() ext-real integer set
[#] (TM | A) is non proper open closed dense Element of bool the carrier of (TM | A)
the carrier of (TM | A) is set
bool the carrier of (TM | A) is non empty set
((TM | A),([#] (TM | A))) 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
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
A is Element of bool the carrier of TM
(TM,A) is V89() V90() ext-real integer set
TAN is Element of bool the carrier of (TM | Null)
((TM | Null),TAN) is V89() V90() ext-real integer set
(TM | Null) | TAN is strict TopSpace-like SubSpace of TM | Null
TM | A is strict TopSpace-like SubSpace of TM
(((TM | Null) | TAN)) is V89() V90() ext-real integer set
[#] ((TM | Null) | TAN) is non proper open closed dense Element of bool the carrier of ((TM | Null) | TAN)
the carrier of ((TM | Null) | TAN) is set
bool the carrier of ((TM | Null) | TAN) is non empty set
(((TM | Null) | TAN),([#] ((TM | Null) | TAN))) is V89() V90() ext-real integer set
((TM | A)) is V89() V90() ext-real integer set
[#] (TM | A) is non proper open closed dense Element of bool the carrier of (TM | A)
the carrier of (TM | A) is set
bool the carrier of (TM | A) is non empty set
((TM | A),([#] (TM | A))) is V89() V90() ext-real integer set
TM is TopSpace-like TopStruct
Null is TopSpace-like TopStruct
(Null) is V89() V90() ext-real integer set
[#] Null is non proper open closed dense Element of bool the carrier of Null
the carrier of Null is set
bool the carrier of Null is non empty set
(Null,([#] Null)) is V89() V90() ext-real integer set
(TM) is V89() V90() ext-real integer set
[#] 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) + 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 set
TAN + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT
A9 is TopSpace-like TopStruct
B is TopSpace-like TopStruct
(A9) is V89() V90() ext-real integer set
[#] A9 is non proper open closed dense Element of bool the carrier of A9
the carrier of A9 is set
bool the carrier of A9 is non empty set
(A9,([#] A9)) is V89() V90() ext-real integer set
(B) is V89() V90() ext-real integer set
[#] B is non proper open closed dense Element of bool the carrier of B
the carrier of B is set
bool the carrier of B is non empty set
(B,([#] B)) is V89() V90() ext-real integer set
[: the carrier of A9, the carrier of B:] is Relation-like set
bool [: the carrier of A9, the carrier of B:] is non empty set
i is Relation-like the carrier of A9 -defined the carrier of B -valued Function-like quasi_total Element of bool [: the carrier of A9, the carrier of B:]
i " is Relation-like the carrier of B -defined the carrier of A9 -valued Function-like quasi_total Element of bool [: the carrier of B, the carrier of A9:]
[: the carrier of B, the carrier of A9:] is Relation-like set
bool [: the carrier of B, the carrier of A9:] is non empty set
dom i is Element of bool the carrier of A9
rng i is Element of bool the carrier of B
{} A9 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 (A9) Element of bool the carrier of A9
{} A9 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 (A9) Element of bool the carrier of A9
b is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
dom (i ") is Element of bool the carrier of B
(TAN + 1) - 1 is V89() V90() ext-real integer Element of REAL
A is Element of the carrier of B
g is open Element of bool the carrier of B
(i ") . A is set
(i ") .: g is Element of bool the carrier of A9
i " g is Element of bool the carrier of A9
h is open Element of bool the carrier of A9
Fr h is closed boundary nowhere_dense Element of bool the carrier of A9
Cl h is closed Element of bool the carrier of A9
h ` is closed Element of bool the carrier of A9
the carrier of A9 \ h is set
Cl (h `) is closed Element of bool the carrier of A9
(Cl h) /\ (Cl (h `)) is closed Element of bool the carrier of A9
(A9,(Fr h)) is V89() V90() ext-real integer set
A9 | (Fr h) is strict TopSpace-like SubSpace of A9
((A9 | (Fr h))) is V89() V90() ext-real integer set
[#] (A9 | (Fr h)) is non proper open closed dense Element of bool the carrier of (A9 | (Fr h))
the carrier of (A9 | (Fr h)) is set
bool the carrier of (A9 | (Fr h)) is non empty set
((A9 | (Fr h)),([#] (A9 | (Fr h)))) is V89() V90() ext-real integer set
i .: (Fr h) is Element of bool the carrier of B
B | (i .: (Fr h)) is strict TopSpace-like SubSpace of B
p is Relation-like Function-like set
p " is Relation-like Function-like set
i . ((i ") . A) is set
((B | (i .: (Fr h)))) is V89() V90() ext-real integer set
[#] (B | (i .: (Fr h))) is non proper open closed dense Element of bool the carrier of (B | (i .: (Fr h)))
the carrier of (B | (i .: (Fr h))) is set
bool the carrier of (B | (i .: (Fr h))) is non empty set
((B | (i .: (Fr h))),([#] (B | (i .: (Fr h))))) is V89() V90() ext-real integer set
i .: h is Element of bool the carrier of B
RngG is open Element of bool the carrier of B
Fr RngG is closed boundary nowhere_dense Element of bool the carrier of B
Cl RngG is closed Element of bool the carrier of B
RngG ` is closed Element of bool the carrier of B
the carrier of B \ RngG is set
Cl (RngG `) is closed Element of bool the carrier of B
(Cl RngG) /\ (Cl (RngG `)) is closed Element of bool the carrier of B
(B,(Fr RngG)) is V89() V90() ext-real integer set
i .: (i " g) is Element of bool the carrier of B
(Cl h) \ h is Element of bool the carrier of A9
i .: ((Cl h) \ h) is Element of bool the carrier of B
i .: (Cl h) is Element of bool the carrier of B
(i .: (Cl h)) \ RngG is Element of bool the carrier of B
(Cl RngG) \ RngG is Element of bool the carrier of B
b is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
{} A9 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 (A9) Element of bool the carrier of A9
TAN is TopSpace-like TopStruct
N9 is TopSpace-like TopStruct
(TAN) is V89() V90() ext-real integer set
[#] TAN is non proper open closed dense Element of bool the carrier of TAN
the carrier of TAN is set
bool the carrier of TAN is non empty set
(TAN,([#] TAN)) is V89() V90() ext-real integer set
(N9) is V89() V90() ext-real integer set
[#] N9 is non proper open closed dense Element of bool the carrier of N9
the carrier of N9 is set
bool the carrier of N9 is non empty set
(N9,([#] N9)) is V89() V90() ext-real integer set
[: the carrier of TAN, the carrier of N9:] is Relation-like set
bool [: the carrier of TAN, the carrier of N9:] is non empty set
A9 is Relation-like the carrier of TAN -defined the carrier of N9 -valued Function-like quasi_total Element of bool [: the carrier of TAN, the carrier of N9:]
A9 " is Relation-like the carrier of N9 -defined the carrier of TAN -valued Function-like quasi_total Element of bool [: the carrier of N9, the carrier of TAN:]
[: the carrier of N9, the carrier of TAN:] is Relation-like set
bool [: the carrier of N9, the carrier of TAN:] is non empty set
dom A9 is Element of bool the carrier of TAN
rng A9 is Element of bool the carrier of N9
{} TAN 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 (TAN) Element of bool the carrier of TAN
{} TAN 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 (TAN) Element of bool the carrier of TAN
i is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
dom (A9 ") is Element of bool the carrier of N9
0 - 1 is V89() V90() ext-real integer Element of REAL
b is Element of the carrier of N9
p is open Element of bool the carrier of N9
(A9 ") . b is set
(A9 ") .: p is Element of bool the carrier of TAN
i1 is Relation-like Function-like set
i1 " is Relation-like Function-like set
A9 . ((A9 ") . b) is set
A9 " p is Element of bool the carrier of TAN
A is open Element of bool the carrier of TAN
Fr A is closed boundary nowhere_dense Element of bool the carrier of TAN
Cl A is closed Element of bool the carrier of TAN
A ` is closed Element of bool the carrier of TAN
the carrier of TAN \ A is set
Cl (A `) is closed Element of bool the carrier of TAN
(Cl A) /\ (Cl (A `)) is closed Element of bool the carrier of TAN
(TAN,(Fr A)) is V89() V90() ext-real integer set
A9 .: A is Element of bool the carrier of N9
g is open Element of bool the carrier of N9
Fr g is closed boundary nowhere_dense Element of bool the carrier of N9
Cl g is closed Element of bool the carrier of N9
g ` is closed Element of bool the carrier of N9
the carrier of N9 \ g is set
Cl (g `) is closed Element of bool the carrier of N9
(Cl g) /\ (Cl (g `)) is closed Element of bool the carrier of N9
(N9,(Fr g)) is V89() V90() ext-real integer set
A9 .: (A9 " p) is Element of bool the carrier of N9
{} N9 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 (N9) Element of bool the carrier of N9
{} TAN 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 (TAN) Element of bool the carrier of TAN
(TM) + 0 is V89() V90() ext-real integer Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
TM is TopSpace-like TopStruct
Null is TopSpace-like TopStruct
(Null) is V89() V90() ext-real integer set
[#] Null is non proper open closed dense Element of bool the carrier of Null
the carrier of Null is set
bool the carrier of Null is non empty set
(Null,([#] Null)) is V89() V90() ext-real integer set
(TM) is V89() V90() ext-real integer set
[#] 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
[: the carrier of TM, the carrier of Null:] is Relation-like set
bool [: the carrier of TM, the carrier of Null:] is non empty set
A is Relation-like the carrier of TM -defined the carrier of Null -valued Function-like quasi_total Element of bool [: the carrier of TM, the carrier of Null:]
dom A is Element of bool the carrier of TM
rng A is Element of bool the carrier of 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 (TM) Element of bool the carrier of TM
N9 is non empty TopSpace-like TopStruct
TAN is non empty TopSpace-like TopStruct
{} 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 epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
TM - 1 is V89() V90() ext-real integer Element of REAL
Null is non empty TopSpace-like TopStruct
(Null) is V89() V90() ext-real integer set
[#] Null is non empty non proper open closed dense non boundary Element of bool the carrier of Null
the carrier of Null is non empty set
bool the carrier of Null is non empty set
(Null,([#] Null)) is V89() V90() ext-real integer set
TAN is Element of the carrier of Null
A is closed Element of bool the carrier of Null
A ` is open Element of bool the carrier of Null
the carrier of Null \ A is set
N9 is Element of bool the carrier of Null
A9 is Element of bool the carrier of Null
A9 ` is Element of bool the carrier of Null
the carrier of Null \ A9 is set
B is open Element of bool the carrier of Null
Fr B is closed boundary nowhere_dense Element of bool the carrier of Null
Cl B is closed Element of bool the carrier of Null
B ` is closed Element of bool the carrier of Null
the carrier of Null \ B is set
Cl (B `) is closed Element of bool the carrier of Null
(Cl B) /\ (Cl (B `)) is closed Element of bool the carrier of Null
(Null,(Fr B)) is V89() V90() ext-real integer set
i is closed boundary nowhere_dense Element of bool the carrier of Null
(Cl B) \ B is Element of bool the carrier of Null
((Cl B) \ B) ` is Element of bool the carrier of Null
the carrier of Null \ ((Cl B) \ B) is set
(((Cl B) \ B) `) ` is Element of bool the carrier of Null
the carrier of Null \ (((Cl B) \ B) `) is set
([#] Null) \ (Cl B) is Element of bool the carrier of Null
([#] Null) /\ B is open Element of bool the carrier of Null
(([#] Null) \ (Cl B)) \/ (([#] Null) /\ B) is Element of bool the carrier of Null
((([#] Null) \ (Cl B)) \/ (([#] Null) /\ B)) ` is Element of bool the carrier of Null
the carrier of Null \ ((([#] Null) \ (Cl B)) \/ (([#] Null) /\ B)) is set
(Cl B) ` is open Element of bool the carrier of Null
the carrier of Null \ (Cl B) is set
((Cl B) `) \/ B is open Element of bool the carrier of Null
(((Cl B) `) \/ B) ` is closed Element of bool the carrier of Null
the carrier of Null \ (((Cl B) `) \/ B) is set
Cl N9 is closed Element of bool the carrier of Null
{TAN} is non empty trivial finite 1 -element compact (Null) Element of bool the carrier of Null
(Null,i) is V89() V90() ext-real integer set
A is Element of the carrier of Null
TAN is open Element of bool the carrier of Null
TAN ` is closed Element of bool the carrier of Null
the carrier of Null \ TAN is set
{A} is non empty trivial finite 1 -element compact (Null) Element of bool the carrier of Null
N9 is Element of bool the carrier of Null
(Null,N9) is V89() V90() ext-real integer set
A9 is open Element of bool the carrier of Null
B is open Element of bool the carrier of Null
A9 \/ B is open Element of bool the carrier of Null
(A9 \/ B) ` is closed Element of bool the carrier of Null
the carrier of Null \ (A9 \/ B) is set
B ` is closed Element of bool the carrier of Null
the carrier of Null \ B is set
Fr A9 is closed boundary nowhere_dense Element of bool the carrier of Null
Cl A9 is closed Element of bool the carrier of Null
A9 ` is closed Element of bool the carrier of Null
the carrier of Null \ A9 is set
Cl (A9 `) is closed Element of bool the carrier of Null
(Cl A9) /\ (Cl (A9 `)) is closed Element of bool the carrier of Null
(Null,(Fr A9)) is V89() V90() ext-real integer set
(Cl A9) \ B is Element of bool the carrier of Null
((Cl A9) \ B) \ A9 is Element of bool the carrier of Null
B \/ A9 is open Element of bool the carrier of Null
(Cl A9) \ (B \/ A9) is Element of bool the carrier of Null
TM is TopSpace-like TopStruct
Null is TopSpace-like TopStruct
TM is TopSpace-like TopStruct
Null is TopSpace-like TopStruct
(TM) is V89() V90() ext-real integer set
[#] 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
(Null) is V89() V90() ext-real integer set
[#] Null is non proper open closed dense Element of bool the carrier of Null
the carrier of Null is set
bool the carrier of Null is non empty set
(Null,([#] Null)) 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
Null is TopSpace-like TopStruct
the carrier of Null is set
bool the carrier of Null is non empty set
A is Element of bool the carrier of TM
TAN is Element of bool the carrier of Null
TM | A is strict TopSpace-like SubSpace of TM
Null | TAN is strict TopSpace-like SubSpace of Null
TM is TopSpace-like TopStruct
the carrier of TM is set
bool the carrier of TM is non empty set
Null is TopSpace-like TopStruct
the carrier of Null is set
bool the carrier of Null is non empty set
A is Element of bool the carrier of TM
(TM,A) is V89() V90() ext-real integer set
TAN is Element of bool the carrier of Null
(Null,TAN) is V89() V90() ext-real integer set
TM | A is strict TopSpace-like SubSpace of TM
Null | TAN is strict TopSpace-like SubSpace of Null
((TM | A)) is V89() V90() ext-real integer set
[#] (TM | A) is non proper open closed dense Element of bool the carrier of (TM | A)
the carrier of (TM | A) is set
bool the carrier of (TM | A) is non empty set
((TM | A),([#] (TM | A))) is V89() V90() ext-real integer set
((Null | TAN)) is V89() V90() ext-real integer set
[#] (Null | TAN) is non proper open closed dense Element of bool the carrier of (Null | TAN)
the carrier of (Null | TAN) is set
bool the carrier of (Null | TAN) is non empty set
((Null | TAN),([#] (Null | TAN))) is V89() V90() ext-real integer set
TM is TopSpace-like TopStruct
Null is TopSpace-like TopStruct
[:TM,Null:] is strict TopSpace-like TopStruct
[:Null,TM:] is strict TopSpace-like TopStruct
([:TM,Null:]) is V89() V90() ext-real integer set
[#] [:TM,Null:] is non proper open closed dense Element of bool the carrier of [:TM,Null:]
the carrier of [:TM,Null:] is set
bool the carrier of [:TM,Null:] is non empty set
([:TM,Null:],([#] [:TM,Null:])) is V89() V90() ext-real integer set
([:Null,TM:]) is V89() V90() ext-real integer set
[#] [:Null,TM:] is non proper open closed dense Element of bool the carrier of [:Null,TM:]
the carrier of [:Null,TM:] is set
bool the carrier of [:Null,TM:] is non empty set
([:Null,TM:],([#] [:Null,TM:])) 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 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 (bool the carrier of (TM | Null)) is non empty 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 (bool the carrier of (TM | Null))
((TM | Null),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
A9 is Element of bool the carrier of (TM | Null)
((TM | Null),A9) is V89() V90() ext-real integer set
N9 is Element of bool the carrier of (TM | Null)
((TM | Null),N9) is V89() V90() ext-real integer set
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 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 (bool the carrier of (TM | Null)) is non empty 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 (bool the carrier of (TM | Null))
((TM | Null),TAN) is V89() V90() ext-real integer set
N9 is Element of bool the carrier of (TM | Null)
((TM | Null),N9) is V89() V90() ext-real integer set
A9 is Element of bool the carrier of TM
(TM,A9) 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
A9 is Element of bool the carrier of (TM | Null)
((TM | Null),A9) is V89() V90() ext-real integer set
TM is TopSpace-like TopStruct
(TM) is V89() V90() ext-real integer set
[#] 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
bool (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
the topology of TM is non empty open 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
[: the carrier of TM, the topology of TM:] is Relation-like set
N9 is set
A9 is set
B is set
[A9,B] is V15() set
{A9,B} is finite set
{A9} is non empty trivial finite 1 -element set
{{A9,B},{A9}} is finite V32() set
i is Element of the carrier of TM
i1 is open Element of bool the carrier of TM
b is Element of the carrier of TM
p is Element of bool the carrier of TM
[b,p] is V15() set
{b,p} is finite set
{b} is non empty trivial finite 1 -element set
{{b,p},{b}} is finite V32() set
i is Element of the carrier of TM
i1 is open Element of bool the carrier of TM
b is open Element of bool the carrier of TM
Fr b is closed boundary nowhere_dense Element of bool the carrier of TM
Cl b is closed Element of bool the carrier of TM
b ` is closed 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
(Cl b) /\ (Cl (b `)) is closed Element of bool the carrier of TM
(TM,(Fr b)) is V89() V90() ext-real integer set
p is Element of the carrier of TM
A is Element of bool the carrier of TM
[p,A] is V15() set
{p,A} is finite set
{p} is non empty trivial finite 1 -element set
{{p,A},{p}} is finite V32() set
i is Element of the carrier of TM
i1 is open Element of bool the carrier of TM
N9 is Relation-like Function-like set
dom N9 is set
rng N9 is set
A9 is set
B is set
N9 . B is set
i is set
i1 is set
[i,i1] is V15() set
{i,i1} is finite set
{i} is non empty trivial finite 1 -element set
{{i,i1},{i}} is finite V32() set
B is Element of bool the carrier of TM
i is Element of the carrier of TM
[i,B] is V15() set
{i,B} is finite set
{i} is non empty trivial finite 1 -element set
{{i,B},{i}} is finite V32() set
N9 . [i,B] is set
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 Element of bool the carrier of TM
p is Element of bool the carrier of TM
A9 is Element of bool (bool the carrier of TM)
B is open V91(TM) Element of bool (bool the carrier of TM)
i1 is Element of bool the carrier of TM
i is open V91(TM) Element of bool (bool the carrier of TM)
b is set
N9 . b is set
p is set
A is set
[p,A] is V15() set
{p,A} is finite set
{p} is non empty trivial finite 1 -element set
{{p,A},{p}} is finite V32() set
N9 . [p,A] is set
Fr i1 is closed Element of bool the carrier of TM
Cl i1 is closed Element of bool the carrier of TM
i1 ` is 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
g is open Element of bool the carrier of TM
Fr g is closed boundary nowhere_dense Element of bool the carrier of TM
Cl g is closed Element of bool the carrier of TM
g ` is closed Element of bool the carrier of TM
the carrier of TM \ g is set
Cl (g `) is closed Element of bool the carrier of TM
(Cl g) /\ (Cl (g `)) is closed Element of bool the carrier of TM
(TM,(Fr g)) is V89() V90() ext-real integer set
Fr i1 is closed Element of bool the carrier of TM
Cl i1 is closed Element of bool the carrier of TM
i1 ` is 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
0 - 1 is V89() V90() ext-real integer Element of REAL
(TM,(Fr i1)) is V89() V90() ext-real integer set
N9 is open V91(TM) Element of bool (bool the carrier of TM)
A9 is Element of the carrier of TM
B is open Element of bool the carrier of TM
i is Element of bool the carrier of TM
i1 is open Element of bool the carrier of TM
b is open Element of bool the carrier of TM
Fr b is closed boundary nowhere_dense Element of bool the carrier of TM
Cl b is closed Element of bool the carrier of TM
b ` is closed 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
(Cl b) /\ (Cl (b `)) is closed Element of bool the carrier of TM
(TM,(Fr b)) 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
[#] TM is non proper open closed dense Element of bool the carrier of TM
(TM) is V89() V90() ext-real integer set
(TM,([#] TM)) is V89() V90() ext-real integer set
Null is Element of the carrier of TM
A is open Element of bool the carrier of TM
{Null} is non empty trivial finite 1 -element set
A ` is closed Element of bool the carrier of TM
the carrier of TM \ A is set
TAN is Element of bool the carrier of TM
N9 is closed Element of bool the carrier of TM
A9 is closed Element of bool the carrier of TM
N9 \/ A9 is closed Element of bool the carrier of TM
A9 ` is open Element of bool the carrier of TM
the carrier of TM \ A9 is set
B is open Element of bool the carrier of TM
(A `) ` is open Element of bool the carrier of TM
the carrier of TM \ (A `) is set
i is open Element of bool the carrier of TM
N9 ` is open Element of bool the carrier of TM
the carrier of TM \ N9 is set
Fr A9 is closed boundary nowhere_dense Element of bool the carrier of TM
Cl A9 is closed Element of bool the carrier of TM
Cl (A9 `) is closed Element of bool the carrier of TM
(Cl A9) /\ (Cl (A9 `)) is closed Element of 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
Fr i is closed boundary nowhere_dense Element of bool the carrier of TM
Cl i is closed Element of bool the carrier of TM
i ` is closed Element of bool the carrier of TM
the carrier of TM \ i is set
Cl (i `) is closed Element of bool the carrier of TM
(Cl i) /\ (Cl (i `)) is closed Element of bool the carrier of TM
(TM,(Fr i)) is V89() V90() ext-real integer set
0 - 1 is V89() V90() ext-real integer Element of REAL
TM is set
bool TM is non empty Element of bool (bool TM)
bool TM is non empty set
bool (bool TM) is non empty set
[:NAT,(bool TM):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool TM):] is non empty non trivial non finite set
Null is non empty Relation-like NAT -defined bool TM -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool TM):]
rng Null is non empty Element of bool (bool TM)
bool (bool TM) is non empty set
union (rng Null) is Element of bool TM
A is set
TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : b₁ in TAN } is set
A9 is set
B is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
Null . B is Element of bool TM
Null . TAN is Element of bool TM
A9 is finite Element of bool (bool TM)
union A9 is Element of bool TM
(Null . TAN) \ (union A9) is Element of bool TM
B is Element of bool TM
i is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
{ (Null . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : not i <= b₁ } is set
Null . i is Element of bool TM
{ (Null . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : not TAN <= b₁ } is set
(Null . i) \ (union A9) is Element of bool TM
b is set
p is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
Null . p is Element of bool TM
b is set
p is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
Null . p is Element of bool TM
A is non empty Relation-like NAT -defined bool TM -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool TM):]
rng A is non empty Element of bool (bool TM)
union (rng A) is Element of bool TM
TAN is set
N9 is set
dom Null is non empty Element of bool NAT
A9 is set
Null . A9 is set
A9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
Null . A9 is Element of bool TM
{ (Null . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : not A9 <= b₁ } is set
A . A9 is Element of bool TM
B is finite Element of bool (bool TM)
union B is Element of bool TM
(Null . A9) \ (union B) is Element of bool TM
i is set
i1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
Null . i1 is Element of bool TM
dom A is non empty Element of bool NAT
TAN is set
N9 is set
dom A is non empty Element of bool NAT
A9 is set
A . A9 is set
B is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
{ (Null . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : not B <= b₁ } is set
A . B is Element of bool TM
Null . B is Element of bool TM
i is finite Element of bool (bool TM)
union i is Element of bool TM
(Null . B) \ (union i) is Element of bool TM
dom Null is non empty Element of bool NAT
N9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
A . TAN is Element of bool TM
A . N9 is Element of bool TM
{ (Null . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : not N9 <= b₁ } is set
Null . N9 is Element of bool TM
A9 is finite Element of bool (bool TM)
union A9 is Element of bool TM
(Null . N9) \ (union A9) is Element of bool TM
B is set
{ (Null . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : not TAN <= b₁ } is set
Null . TAN is Element of bool TM
i is finite Element of bool (bool TM)
union i is Element of bool TM
(Null . TAN) \ (union i) is Element of bool TM
TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
N9 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
A . TAN is Element of bool TM
A . N9 is Element of bool TM
TAN is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
{ (Null . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : not TAN <= b₁ } is set
A . TAN is Element of bool TM
Null . TAN is Element of bool TM
TM is TopSpace-like TopStruct
(TM) is V89() V90() ext-real integer set
[#] 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
A is closed Element of bool the carrier of TM
TAN is closed Element of bool the carrier of TM
A \/ TAN is closed Element of bool the carrier of TM
A ` is open Element of bool the carrier of TM
the carrier of TM \ A is set
TAN ` is open Element of bool the carrier of TM
the carrier of TM \ TAN is set
bool ([#] TM) is non empty Element of bool (bool ([#] TM))
bool ([#] TM) is non empty set
bool (bool ([#] TM)) is non empty set
N9 is set
A9 is Element of the carrier of TM
0 - 1 is V89() V90() ext-real integer Element of REAL
B is open Element of bool the carrier of TM
Fr B is closed boundary nowhere_dense Element of bool the carrier of TM
Cl B is closed Element of bool the carrier of TM
B ` is closed 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
(Cl B) /\ (Cl (B `)) is closed Element of bool the carrier of TM
(TM,(Fr B)) is V89() V90() ext-real integer 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
A9 is Element of the carrier of TM
0 - 1 is V89() V90() ext-real integer Element of REAL
B is open Element of bool the carrier of TM
Fr B is closed boundary nowhere_dense Element of bool the carrier of TM
Cl B is closed Element of bool the carrier of TM
B ` is closed 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
(Cl B) /\ (Cl (B `)) is closed Element of bool the carrier of TM
(TM,(Fr B)) is V89() V90() ext-real integer 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
A9 is Element of the carrier of TM
[:([#] TM),(bool ([#] TM)):] is Relation-like set
bool [:([#] TM),(bool ([#] TM)):] is non empty set
N9 is Relation-like [#] TM -defined bool ([#] TM) -valued Function-like V14( [#] TM) quasi_total Element of bool [:([#] TM),(bool ([#] TM)):]
bool (bool the carrier of TM) is non empty set
rng N9 is Element of bool (bool ([#] TM))
bool (bool ([#] TM)) is non empty set
dom N9 is Element of bool ([#] TM)
A9 is Element of bool (bool the carrier of TM)
union A9 is Element of bool the carrier of TM
B is set
i is Element of the carrier of TM
N9 . i is set
B is Element of bool the carrier of TM
i is set
N9 . i is set
B is Element of bool (bool the carrier of TM)
[:NAT,B:] is Relation-like set
bool [:NAT,B:] is non empty set
i is Relation-like NAT -defined B -valued Function-like quasi_total Element of bool [:NAT,B:]
rng i is Element of bool B
bool B is non empty set
dom i is Element of bool NAT
[:NAT,(bool ([#] TM)):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool ([#] TM)):] is non empty non trivial non finite set
i1 is non empty Relation-like NAT -defined bool ([#] TM) -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool ([#] TM)):]
rng i1 is non empty Element of bool (bool ([#] TM))
union (rng i1) is Element of bool ([#] TM)
b is non empty Relation-like NAT -defined bool ([#] TM) -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool ([#] TM)):]
rng b is non empty Element of bool (bool ([#] TM))
union (rng b) is Element of bool ([#] TM)
{ (b . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : b . b₁ misses TAN } is set
g is set
dom b is non empty Element of bool NAT
h is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
b . h is Element of bool ([#] TM)
p is Element of bool (bool the carrier of TM)
g is Element of bool (bool the carrier of TM)
p \ g is Element of bool (bool the carrier of TM)
RngH is Element of bool the carrier of TM
dom b is non empty Element of bool NAT
RngG is set
b . RngG is set
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
{ (i1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : not unionG <= b₁ } is set
b . unionG is Element of bool ([#] TM)
i1 . unionG is Element of bool ([#] TM)
unionH is finite Element of bool (bool ([#] TM))
union unionH is Element of bool ([#] TM)
(i1 . unionG) \ (union unionH) is Element of bool ([#] TM)
unionG is set
N9 . unionG is set
unionG is Element of bool (bool the carrier of TM)
unionG is Element of bool the carrier of TM
unionH is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
i1 . unionH is Element of bool ([#] TM)
unionH is set
N9 . unionH is set
union unionG is Element of bool the carrier of TM
unionH is open Element of bool the carrier of TM
(union unionG) ` is Element of bool the carrier of TM
the carrier of TM \ (union unionG) is set
unionH /\ ((union unionG) `) is Element of bool the carrier of TM
union g is Element of bool the carrier of TM
union (p \ g) is Element of bool the carrier of TM
RngH is open Element of bool the carrier of TM
RngG is open Element of bool the carrier of TM
unionG is set
unionH is set
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
b . unionG is Element of bool ([#] TM)
unionH is set
dom b is non empty Element of bool NAT
unionG is set
b . unionG is set
unionH is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
b . unionH is Element of bool ([#] TM)
(p \ g) \/ g is Element of bool (bool the carrier of TM)
RngH \/ RngG is open Element of bool the carrier of TM
union B is Element of bool the carrier of TM
RngG ` is closed Element of bool the carrier of TM
the carrier of TM \ RngG is set
unionG is set
unionH is set
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
b . unionG is Element of bool ([#] TM)
RngH ` is closed Element of bool the carrier of TM
the carrier of TM \ RngH is set
unionG is set
unionH is set
dom b is non empty Element of bool NAT
unionG is set
b . unionG is set
unionH is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
b . unionH is Element of bool ([#] TM)
unionG is set
i1 . unionH is Element of bool ([#] TM)
unionH is set
N9 . unionH is set
{ (i1 . b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : not unionH <= b₁ } is set
U is finite Element of bool (bool ([#] TM))
union U is Element of bool ([#] TM)
(i1 . unionH) \ (union U) is Element of bool ([#] TM)
n is Element of bool the carrier of TM
U is finite Element of bool (bool ([#] TM))
union U is Element of bool ([#] TM)
(i1 . unionH) \ (union U) is Element of bool ([#] TM)
TM is TopSpace-like TopStruct
(TM) is V89() V90() ext-real integer set
[#] 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 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
Null is closed Element of bool the carrier of TM
A is closed Element of bool the carrier of TM
TAN is closed Element of bool the carrier of TM
N9 is closed Element of bool the carrier of TM
TAN \/ N9 is closed Element of bool the carrier of TM
TAN ` is open Element of bool the carrier of TM
the carrier of TM \ TAN is set
(TAN \/ N9) ` is open Element of bool the carrier of TM
the carrier of TM \ (TAN \/ N9) is set
({} TM) ` is open closed dense Element of bool the carrier of TM
the carrier of TM \ ({} TM) is set
(({} TM) `) ` is open closed Element of bool the carrier of TM
the carrier of TM \ (({} TM) `) is set
N9 ` is open Element of bool the carrier of TM
the carrier of TM \ N9 is set
Null is closed Element of bool the carrier of TM
A is closed 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
TAN \/ N9 is open Element of bool the carrier of TM
(TAN \/ N9) ` is closed Element of bool the carrier of TM
the carrier of TM \ (TAN \/ N9) is set
((TAN \/ N9) `) ` is open Element of bool the carrier of TM
the carrier of TM \ ((TAN \/ N9) `) is set
N9 ` is closed Element of bool the carrier of TM
the carrier of TM \ N9 is set
TAN ` is closed Element of bool the carrier of TM
the carrier of TM \ TAN is 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 V89() V90() ext-real integer set
[#] TM is non proper open closed dense Element of bool the carrier of TM
(TM,([#] TM)) 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
union A is Element of 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
union A is Element of bool the carrier of TM
[:NAT,A:] is Relation-like set
bool [:NAT,A:] is non empty set
N9 is Relation-like NAT -defined A -valued Function-like quasi_total Element of bool [:NAT,A:]
rng N9 is Element of bool A
bool A is non empty set
dom N9 is Element of bool NAT
TAN is non empty set
bool TAN is non empty Element of bool (bool TAN)
bool TAN is non empty set
bool (bool TAN) is non empty set
[:(bool TAN),(bool TAN):] is non empty Relation-like set
the topology of TM is non empty open Element of bool (bool the carrier of TM)
i is closed Element of bool the carrier of TM
i1 is closed Element of bool the carrier of TM
Cl i is closed Element of bool the carrier of TM
Cl i1 is closed Element of bool the carrier of TM
[:NAT,[:(bool TAN),(bool TAN):]:] is non empty non trivial Relation-like non finite set
b is set
p is set
A is set
[p,A] is V15() set
{p,A} is finite set
{p} is non empty trivial finite 1 -element set
{{p,A},{p}} is finite V32() set
g is set
h is set
[g,h] is V15() set
{g,h} is finite set
{g} is non empty trivial finite 1 -element set
{{g,h},{g}} is finite V32() set
RngH is Element of bool the carrier of TM
Cl RngH is closed Element of bool the carrier of TM
RngG is Element of bool the carrier of TM
Cl RngG is closed Element of bool the carrier of TM
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
N9 . unionG is Element of A
unionH is Element of bool the carrier of TM
Cl unionH is closed Element of bool the carrier of TM
unionG is Element of bool the carrier of TM
[unionH,unionG] is V15() Element of [:(bool the carrier of TM),(bool the carrier of TM):]
[:(bool the carrier of TM),(bool the carrier of TM):] is non empty Relation-like set
{unionH,unionG} is finite set
{unionH} is non empty trivial finite 1 -element set
{{unionH,unionG},{unionH}} is finite V32() set
[unionG,[unionH,unionG]] is V15() set
{unionG,[unionH,unionG]} is finite set
{unionG} is non empty trivial finite V32() 1 -element set
{{unionG,[unionH,unionG]},{unionG}} is finite V32() set
Cl unionG is closed Element of bool the carrier of TM
RngH is Element of bool the carrier of TM
Cl RngH is closed Element of bool the carrier of TM
RngG is Element of bool the carrier of TM
Cl RngG is closed Element of bool the carrier of TM
N9 . p is set
unionG is Element of bool the carrier of TM
TM | unionG is strict TopSpace-like SubSpace of TM
((TM | unionG)) is V89() V90() ext-real integer set
[#] (TM | unionG) is non proper open closed dense Element of bool the carrier of (TM | unionG)
the carrier of (TM | unionG) is set
bool the carrier of (TM | unionG) is non empty set
((TM | unionG),([#] (TM | unionG))) is V89() V90() ext-real integer set
(TM,unionG) is V89() V90() ext-real integer set
(Cl RngH) /\ unionG is Element of bool the carrier of TM
(Cl RngG) /\ unionG is Element of bool the carrier of TM
unionH is Element of bool the carrier of (TM | unionG)
unionG is Element of bool the carrier of (TM | unionG)
unionH is closed Element of bool the carrier of (TM | unionG)
unionG is closed Element of bool the carrier of (TM | unionG)
unionH \/ unionG is closed Element of bool the carrier of (TM | unionG)
unionH is Element of bool the carrier of TM
unionH \/ (Cl RngH) is Element of bool the carrier of TM
n is Element of bool the carrier of TM
n \/ (Cl RngG) is Element of bool the carrier of TM
U is set
U is open Element of bool the carrier of TM
W is open Element of bool the carrier of TM
Cl U is closed Element of bool the carrier of TM
Cl W is closed Element of bool the carrier of TM
[:(bool the carrier of TM),(bool the carrier of TM):] is non empty Relation-like set
[U,W] is V15() Element of [:(bool the carrier of TM),(bool the carrier of TM):]
{U,W} is finite set
{U} is non empty trivial finite 1 -element set
{{U,W},{U}} is finite V32() set
uw is V15() Element of [:(bool the carrier of TM),(bool the carrier of TM):]
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
N9 . n is Element of A
A is Element of bool the carrier of TM
Cl A is closed Element of bool the carrier of TM
B is Element of bool the carrier of TM
[A,B] is V15() Element of [:(bool the carrier of TM),(bool the carrier of TM):]
{A,B} is finite set
{A} is non empty trivial finite 1 -element set
{{A,B},{A}} is finite V32() set
[n,[A,B]] is V15() set
{n,[A,B]} is finite set
{n} is non empty trivial finite V32() 1 -element set
{{n,[A,B]},{n}} is finite V32() set
Cl B is closed Element of bool the carrier of TM
U \/ W is open Element of bool the carrier of TM
RngH is Element of bool the carrier of TM
Cl RngH is closed Element of bool the carrier of TM
RngG is Element of bool the carrier of TM
Cl RngG is closed Element of bool the carrier of TM
b is Relation-like Function-like set
dom b is set
[i,i1] is V15() Element of [:(bool the carrier of TM),(bool the carrier of TM):]
[:(bool the carrier of TM),(bool the carrier of TM):] is non empty Relation-like set
{i,i1} is finite set
{i} is non empty trivial finite 1 -element set
{{i,i1},{i}} is finite V32() set
p is Relation-like Function-like set
dom p is set
p . 0 is set
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
p . A is set
(p . A) `1 is set
(p . A) `2 is 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
p . (A + 1) is set
(p . (A + 1)) `1 is set
(p . (A + 1)) `2 is set
g is set
h is set
[g,h] is V15() set
{g,h} is finite set
{g} is non empty trivial finite 1 -element set
{{g,h},{g}} is finite V32() set
[A,(p . A)] is V15() set
{A,(p . A)} is finite set
{A} is non empty trivial finite V32() 1 -element set
{{A,(p . A)},{A}} is finite V32() set
RngH is Element of bool the carrier of TM
RngG is Element of bool the carrier of TM
[RngH,RngG] is V15() Element of [:(bool the carrier of TM),(bool the carrier of TM):]
{RngH,RngG} is finite set
{RngH} is non empty trivial finite 1 -element set
{{RngH,RngG},{RngH}} is finite V32() set
[RngH,RngG] `1 is Element of bool the carrier of TM
[RngH,RngG] `2 is Element of bool the carrier of TM
Cl RngH is closed Element of bool the carrier of TM
Cl RngG is closed Element of bool the carrier of TM
N9 . A is Element of A
b . [A,(p . A)] is set
unionG is open Element of bool the carrier of TM
unionH is open Element of bool the carrier of TM
unionG \/ unionH is open Element of bool the carrier of TM
[unionG,unionH] is V15() Element of [:(bool the carrier of TM),(bool the carrier of TM):]
{unionG,unionH} is finite set
{unionG} is non empty trivial finite 1 -element set
{{unionG,unionH},{unionG}} is finite V32() set
Cl unionG is closed Element of bool the carrier of TM
Cl unionH is closed Element of bool the carrier of TM
[unionG,unionH] `1 is Element of bool the carrier of TM
[unionG,unionH] `2 is Element of bool the carrier of TM
unionG is Element of bool the carrier of TM
unionH is Element of bool the carrier of TM
Cl unionG is closed Element of bool the carrier of TM
Cl unionH is closed Element of bool the carrier of TM
[i,i1] `1 is Element of bool the carrier of TM
[i,i1] `2 is Element of bool the carrier of TM
(p . 0) `1 is set
(p . 0) `2 is set
A is Element of bool the carrier of TM
g is Element of bool the carrier of TM
Cl A is closed Element of bool the carrier of TM
Cl g is closed Element of bool the carrier of TM
rng p is set
A is set
g is set
p . g is set
bool [:NAT,[:(bool TAN),(bool TAN):]:] is non empty non trivial non finite set
A is non empty Relation-like NAT -defined [:(bool TAN),(bool TAN):] -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,[:(bool TAN),(bool TAN):]:]
pr1 A is non empty Relation-like NAT -defined bool TAN -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool TAN):]
[:NAT,(bool TAN):] is non empty non trivial Relation-like non finite set
bool [:NAT,(bool TAN):] is non empty non trivial non finite set
pr2 A is non empty Relation-like NAT -defined bool TAN -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool TAN):]
(pr2 A) . 0 is Element of bool TAN
(pr2 A) ^\ 1 is non empty Relation-like NAT -defined bool TAN -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool TAN):]
rng ((pr2 A) ^\ 1) is non empty Element of bool (bool TAN)
bool (bool TAN) is non empty set
(pr1 A) ^\ 1 is non empty Relation-like NAT -defined bool TAN -valued Function-like V14( NAT ) quasi_total Element of bool [:NAT,(bool TAN):]
rng ((pr1 A) ^\ 1) is non empty Element of bool (bool TAN)
(pr1 A) . 0 is Element of bool TAN
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
unionG + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT
(pr1 A) . (unionG + 1) is Element of bool TAN
(pr2 A) . (unionG + 1) is Element of bool TAN
(pr1 A) . unionG is Element of bool TAN
(pr2 A) . unionG is Element of bool TAN
N9 . unionG is Element of A
((pr1 A) . (unionG + 1)) \/ ((pr2 A) . (unionG + 1)) is Element of bool TAN
A . unionG is Element of [:(bool TAN),(bool TAN):]
unionH is set
unionG is set
[unionH,unionG] is V15() set
{unionH,unionG} is finite set
{unionH} is non empty trivial finite 1 -element set
{{unionH,unionG},{unionH}} is finite V32() set
[unionG,(A . unionG)] is V15() set
{unionG,(A . unionG)} is finite set
{unionG} is non empty trivial finite V32() 1 -element set
{{unionG,(A . unionG)},{unionG}} is finite V32() set
unionH is Element of bool the carrier of TM
unionG is Element of bool the carrier of TM
[unionH,unionG] is V15() Element of [:(bool the carrier of TM),(bool the carrier of TM):]
{unionH,unionG} is finite set
{unionH} is non empty trivial finite 1 -element set
{{unionH,unionG},{unionH}} is finite V32() set
[unionH,unionG] `1 is Element of bool the carrier of TM
[unionH,unionG] `2 is Element of bool the carrier of TM
Cl unionH is closed Element of bool the carrier of TM
Cl unionG is closed Element of bool the carrier of TM
b . [unionG,(A . unionG)] is set
unionH is open Element of bool the carrier of TM
n is open Element of bool the carrier of TM
unionH \/ n is open Element of bool the carrier of TM
[unionH,n] is V15() Element of [:(bool the carrier of TM),(bool the carrier of TM):]
{unionH,n} is finite set
{unionH} is non empty trivial finite 1 -element set
{{unionH,n},{unionH}} is finite V32() set
Cl unionH is closed Element of bool the carrier of TM
Cl n is closed Element of bool the carrier of TM
A . (unionG + 1) is Element of [:(bool TAN),(bool TAN):]
[unionH,n] `1 is Element of bool the carrier of TM
[unionH,n] `2 is Element of bool the carrier of TM
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
(pr1 A) . unionG is Element of bool TAN
unionG + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT
(pr1 A) . (unionG + 1) is Element of bool TAN
RngH is Element of bool (bool the carrier of TM)
{ ((pr2 A) . b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : 1 <= b<sub>1</sub> } is set
unionG is Element of bool the carrier of TM
unionH is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
(pr2 A) . unionH is Element of bool TAN
unionH - 1 is V89() V90() ext-real integer Element of REAL
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
unionG + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT
(pr2 A) . (unionG + 1) is Element of bool TAN
RngG is Element of bool (bool the carrier of TM)
{ ((pr1 A) . b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : 1 <= b<sub>1</sub> } is set
unionG is Element of bool the carrier of TM
unionH is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
(pr1 A) . unionH is Element of bool TAN
unionH - 1 is V89() V90() ext-real integer Element of REAL
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer set
unionG + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT
(pr1 A) . (unionG + 1) is Element of bool TAN
union RngG is Element of bool the carrier of TM
union RngH is Element of bool the carrier of TM
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
(pr2 A) . unionG is Element of bool TAN
unionG + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT
(pr2 A) . (unionG + 1) is Element of bool TAN
unionH is open Element of bool the carrier of TM
unionG is open Element of bool the carrier of TM
unionG is set
unionH is set
{ ((pr2 A) . b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : 1 <= b<sub>1</sub> } is set
unionG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
(pr2 A) . unionG is Element of bool TAN
unionH is set
{ ((pr1 A) . b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : 1 <= b<sub>1</sub> } is set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
(pr1 A) . n is Element of bool TAN
(pr2 A) . n is Element of bool TAN
(pr1 A) . unionG is Element of bool TAN
unionH \/ unionG is open Element of bool the carrier of TM
unionG is set
unionH is Element of the carrier of TM
unionG is set
unionH is set
N9 . unionH is set
n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT
N9 . n is Element of A
(pr1 A) . (n + 1) is Element of bool TAN
(pr2 A) . (n + 1) is Element of bool TAN
((pr1 A) . (n + 1)) \/ ((pr2 A) . (n + 1)) is Element of bool TAN
{ ((pr1 A) . b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : 1 <= b<sub>1</sub> } is set
{ ((pr2 A) . b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : 1 <= b<sub>1</sub> } is set
unionG ` is closed Element of bool the carrier of TM
the carrier of TM \ unionG is set
unionH ` is closed Element of bool the carrier of TM
the carrier of TM \ unionH is set
unionG is closed Element of bool the carrier of TM
unionH is closed Element of bool the carrier of TM
unionG is closed Element of bool the carrier of TM
unionH is closed Element of bool the carrier of TM
unionG \/ unionH is closed Element of bool the carrier of TM
{ ((pr1 A) . b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : 1 <= b<sub>1</sub> } is set
(pr1 A) . 1 is Element of bool TAN
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real positive non negative integer Element of NAT
(pr1 A) . (0 + 1) is Element of bool TAN
{ ((pr2 A) . b<sub>1</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT : 1 <= b<sub>1</sub> } is set
(pr2 A) . 1 is Element of bool TAN
(pr2 A) . (0 + 1) is Element of bool TAN
union A is Element of bool the carrier of TM
TM is TopSpace-like T_0 T_1 normal T_4 metrizable 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 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
A9 is (TM) Element of bool the carrier of TM
(TM,A9) is V89() V90() ext-real integer set
TM | A9 is strict TopSpace-like T_0 T_1 normal T_4 metrizable () SubSpace of TM
[#] (TM | A9) is non proper open closed dense (TM | A9) Element of bool the carrier of (TM | A9)
the carrier of (TM | A9) is set
bool the carrier of (TM | A9) is non empty set
(Cl TAN) /\ A9 is Element of bool the carrier of TM
(Cl N9) /\ A9 is Element of bool the carrier of TM
i is (TM | A9) Element of bool the carrier of (TM | A9)
i1 is (TM | A9) Element of bool the carrier of (TM | A9)
((TM | A9)) is V89() V90() ext-real integer set
((TM | A9),([#] (TM | A9))) is V89() V90() ext-real integer set
{} (TM | A9) 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 | A9) Element of bool the carrier of (TM | A9)
b is Element of bool the carrier of TM
A9 /\ b is Element of bool the carrier of TM
TM is TopSpace-like T_0 T_1 normal T_4 metrizable 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
TM | Null is strict TopSpace-like T_0 T_1 normal T_4 metrizable SubSpace of TM
(TM,Null) is V89() V90() ext-real integer set
A is Element of the carrier of TM
TAN is open Element of bool the carrier of TM
{A} is non empty trivial finite 1 -element set
TAN ` is closed Element of bool the carrier of TM
the carrier of TM \ TAN is set
N9 is Element of bool the carrier of TM
A9 is Element of bool the carrier of TM
B is open Element of bool the carrier of TM
i is open Element of bool the carrier of TM
B \/ i is open Element of bool the carrier of TM
(B \/ i) ` is closed Element of bool the carrier of TM
the carrier of TM \ (B \/ i) is set
i1 is open Element of bool the carrier of TM
i ` is closed Element of bool the carrier of TM
the carrier of TM \ i is set
(TAN `) ` is open Element of bool the carrier of TM
the carrier of TM \ (TAN `) is set
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
b is set
A9 ` is Element of bool the carrier of TM
the carrier of TM \ A9 is set
(Cl i1) \ i1 is Element of bool the carrier of TM
the carrier of (TM | Null) is set
bool the carrier of (TM | Null) is non empty set
0 - 1 is V89() V90() ext-real integer Element of REAL
TAN is Element of the carrier of (TM | Null)
N9 is open Element of bool the carrier of (TM | Null)
[#] (TM | Null) is non proper open closed dense Element of bool the carrier of (TM | Null)
B is Element of bool the carrier of TM
B /\ the carrier of (TM | Null) is Element of bool the carrier of TM
A9 is Element of the carrier of TM
i is open Element of bool the carrier of TM
Fr i is closed boundary nowhere_dense Element of bool the carrier of TM
Cl i is closed Element of bool the carrier of TM
i ` is closed Element of bool the carrier of TM
the carrier of TM \ i is set
Cl (i `) is closed Element of bool the carrier of TM
(Cl i) /\ (Cl (i `)) is closed Element of bool the carrier of TM
i /\ the carrier of (TM | Null) is Element of bool the carrier of TM
i1 is Element of bool the carrier of (TM | Null)
b is open Element of bool the carrier of (TM | Null)
Fr b is closed boundary nowhere_dense Element of bool the carrier of (TM | Null)
Cl b is closed Element of bool the carrier of (TM | Null)
b ` is closed Element of bool the carrier of (TM | Null)
the carrier of (TM | Null) \ b is set
Cl (b `) is closed Element of bool the carrier of (TM | Null)
(Cl b) /\ (Cl (b `)) is closed Element of bool the carrier of (TM | Null)
((TM | Null),(Fr b)) is V89() V90() ext-real integer set
(Fr i) /\ Null is Element of bool the carrier of TM
((TM | Null)) is V89() V90() ext-real integer set
[#] (TM | Null) is non proper open closed dense Element of bool the carrier of (TM | Null)
((TM | Null),([#] (TM | Null))) is V89() V90() ext-real integer set
TM is TopSpace-like T_0 T_1 normal T_4 metrizable 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 non proper open closed dense Element of bool the carrier of TM
the topology of TM is non empty open Element of bool (bool the carrier of TM)
TAN is Element of bool the carrier of TM
TM | TAN is strict TopSpace-like T_0 T_1 normal T_4 metrizable SubSpace of TM
(TM,TAN) is V89() V90() ext-real integer 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), the topology of TM:] is Relation-like set
N9 is set
A9 is set
B is set
[A9,B] is V15() set
{A9,B} is finite set
{A9} is non empty trivial finite 1 -element set
{{A9,B},{A9}} is finite V32() set
i is Element of the carrier of TM
i1 is open Element of bool the carrier of TM
b is Element of the carrier of TM
p is Element of bool the carrier of TM
[b,p] is V15() set
{b,p} is finite set
{b} is non empty trivial finite 1 -element set
{{b,p},{b}} is finite V32() set
i is Element of the carrier of TM
i1 is open Element of bool the carrier of TM
b is open Element of bool the carrier of TM
Fr b is closed boundary nowhere_dense Element of bool the carrier of TM
Cl b is closed Element of bool the carrier of TM
b ` is closed 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
(Cl b) /\ (Cl (b `)) is closed Element of bool the carrier of TM
p is Element of the carrier of TM
A is Element of bool the carrier of TM
[p,A] is V15() set
{p,A} is finite set
{p} is non empty trivial finite 1 -element set
{{p,A},{p}} is finite V32() set
i is Element of the carrier of TM
i1 is open Element of bool the carrier of TM
N9 is Relation-like Function-like set
dom N9 is set
rng N9 is set
A9 is set
B is set
N9 . B is set
i is set
i1 is set
[i,i1] is V15() set
{i,i1} is finite set
{i} is non empty trivial finite 1 -element set
{{i,i1},{i}} is finite V32() set
B is Element of bool the carrier of TM
i is Element of the carrier of TM
[i,B] is V15() set
{i,B} is finite set
{i} is non empty trivial finite 1 -element set
{{i,B},{i}} is finite V32() set
N9 . [i,B] is set
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
b is Element of bool the carrier of TM
p is Element of bool the carrier of TM
A9 is Element of bool (bool the carrier of TM)
B is open V91(TM) Element of bool (bool the carrier of TM)
i1 is Element of bool the carrier of TM
i is open V91(TM) Element of bool (bool the carrier of TM)
b is set
N9 . b is set
p is set
A is set
[p,A] is V15() set
{p,A} is finite set
{p} is non empty trivial finite 1 -element set
{{p,A},{p}} is finite V32() set
N9 . [p,A] is set
Fr i1 is closed Element of bool the carrier of TM
Cl i1 is closed Element of bool the carrier of TM
i1 ` is 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
g is open Element of bool the carrier of TM
Fr g is closed boundary nowhere_dense Element of bool the carrier of TM
Cl g is closed Element of bool the carrier of TM
g ` is closed Element of bool the carrier of TM
the carrier of TM \ g is set
Cl (g `) is closed Element of bool the carrier of TM
(Cl g) /\ (Cl (g `)) is closed Element of bool the carrier of TM
Fr i1 is closed Element of bool the carrier of TM
Cl i1 is closed Element of bool the carrier of TM
i1 ` is 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
N9 is open V91(TM) Element of bool (bool the carrier of TM)
A9 is Element of the carrier of TM
B is open Element of bool the carrier of TM
i is 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 is TopSpace-like T_0 T_1 normal T_4 metrizable 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
TM | Null is strict TopSpace-like T_0 T_1 normal T_4 metrizable SubSpace of TM
A is Element of bool the carrier of TM
(TM,Null) is V89() V90() ext-real integer set
A \/ Null is Element of bool the carrier of TM
(TM,(A \/ Null)) is V89() V90() ext-real integer set
(TM,A) is V89() V90() ext-real integer set
(TM,A) + 1 is V89() V90() ext-real integer Element of REAL
TM | (A \/ Null) is strict TopSpace-like T_0 T_1 normal T_4 metrizable SubSpace of TM
[#] (TM | (A \/ Null)) is non proper open closed dense Element of bool the carrier of (TM | (A \/ Null))
the carrier of (TM | (A \/ Null)) is set
bool the carrier of (TM | (A \/ Null)) is non empty set
N9 is Element of bool the carrier of (TM | (A \/ Null))
((TM | (A \/ Null)),N9) is V89() V90() ext-real integer set
(TM | (A \/ Null)) | N9 is strict TopSpace-like T_0 T_1 normal T_4 metrizable SubSpace of TM | (A \/ Null)
bool (bool the carrier of (TM | (A \/ Null))) is non empty set
B is open V91(TM | (A \/ Null)) Element of bool (bool the carrier of (TM | (A \/ Null)))
(- 1) + 1 is V89() V90() ext-real integer Element of REAL
A9 is Element of bool the carrier of (TM | (A \/ Null))
((TM | (A \/ Null)),A9) is V89() V90() ext-real integer set
i1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V89() V90() ext-real non negative integer Element of NAT
i1 - 1 is V89() V90() ext-real integer Element of REAL
b is Element of bool the carrier of (TM | (A \/ Null))
Fr b is closed Element of bool the carrier of (TM | (A \/ Null))
Cl b is closed Element of bool the carrier of (TM | (A \/ Null))
b ` is Element of bool the carrier of (TM | (A \/ Null))
the carrier of (TM | (A \/ Null)) \ b is set
Cl (b `) is closed Element of bool the carrier of (TM | (A \/ Null))
(Cl b) /\ (Cl (b `)) is closed Element of bool the carrier of (TM | (A \/ Null))
((TM | (A \/ Null)),(Fr b)) is V89() V90() ext-real integer set
((TM | (A \/ Null))) is V89() V90() ext-real integer set
((TM | (A \/ Null)),([#] (TM | (A \/ Null)))) is V89() V90() ext-real integer set