:: TOPDIM_1 semantic presentation

REAL is set

bool REAL is non empty 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,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

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

bool is non empty set

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

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

bool is non empty set
bool () is non empty set
bool NAT is non empty non trivial non finite set

RAT is set
INT is set
bool is non empty set
K540(2) is V290() L20()
the carrier of K540(2) is set
{} is set

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

((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 non empty trivial finite V32() 1 -element Element of bool (bool the carrier of (TM | Null))

{({} 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)

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

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

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

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

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

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

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

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

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

(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

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

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

(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 non empty trivial finite V32() 1 -element Element of bool (bool the carrier of A)

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

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)

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

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)

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

((1TopSp TM)) . (0 + 1) is Element of bool (bool the carrier of (1TopSp TM))
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
[#] (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

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

(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

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

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

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

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

(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

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

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

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

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

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

(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

the carrier of TM is set
bool the carrier of TM is non empty 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 - 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)

(TM) . (Null + 1) is Element of bool (bool the carrier of TM)
(Null + 1) - 1 is V89() V90() ext-real integer Element of REAL

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

(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

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)

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

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

(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

(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

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

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

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)

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 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 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 non empty trivial finite V32() 1 -element Element of bool (bool the carrier of (1TopSp TM))

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

the carrier of TM is set
bool the carrier of TM is non empty 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)

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

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