:: KURATO_1 semantic presentation

REAL is V136() V137() V138() V142() set
NAT is V136() V137() V138() V139() V140() V141() V142() Element of bool REAL
bool REAL is non empty set
NAT is V136() V137() V138() V139() V140() V141() V142() set
bool NAT is non empty set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
K228() is V122() TopStruct
the carrier of K228() is V136() V137() V138() set
1 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is non empty set
K256() is V108() V122() L7()
R^1 is non empty strict TopSpace-like V122() TopStruct
COMPLEX is V136() V142() set
RAT is V136() V137() V138() V139() V142() set
INT is V136() V137() V138() V139() V140() V142() set
bool NAT is non empty set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is set
bool [:COMPLEX,REAL:] is non empty set
{} is empty finite V38() V136() V137() V138() V139() V140() V141() V142() set
7 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
the carrier of R^1 is non empty V136() V137() V138() set
6 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
bool the carrier of R^1 is non empty set
+infty is non empty ext-real positive non negative set
-infty is non empty ext-real non positive negative set
4 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
RAT (2,4) is V136() V137() V138() Element of bool REAL
5 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
].4,5.[ is V136() V137() V138() Element of bool REAL
(RAT (2,4)) \/ ].4,5.[ is V136() V137() V138() Element of bool REAL
].5,+infty.[ is non empty V136() V137() V138() Element of bool REAL
((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ is non empty V136() V137() V138() Element of bool REAL
].-infty,2.] is non empty V136() V137() V138() Element of bool REAL
IRRAT (2,4) is V136() V137() V138() Element of bool REAL
].-infty,2.] \/ (IRRAT (2,4)) is non empty V136() V137() V138() Element of bool REAL
{4} is non empty with_non-empty_elements non empty-membered finite V136() V137() V138() V139() V140() V141() Element of bool REAL
(].-infty,2.] \/ (IRRAT (2,4))) \/ {4} is non empty V136() V137() V138() Element of bool REAL
{5} is non empty with_non-empty_elements non empty-membered finite V136() V137() V138() V139() V140() V141() Element of bool REAL
((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} is non empty V136() V137() V138() Element of bool REAL
].-infty,1.[ is non empty V136() V137() V138() Element of bool REAL
].1,+infty.[ is non empty V136() V137() V138() Element of bool REAL
].-infty,1.[ \/ ].1,+infty.[ is non empty V136() V137() V138() Element of bool REAL
(].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) is V136() V137() V138() Element of bool REAL
].1,2.] is V136() V137() V138() Element of bool REAL
].-infty,1.[ \/ ].1,2.] is non empty V136() V137() V138() Element of bool REAL
(].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4)) is non empty V136() V137() V138() Element of bool REAL
((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4} is non empty V136() V137() V138() Element of bool REAL
(((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5} is non empty V136() V137() V138() Element of bool REAL
K146(-infty,+infty) is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
Cl c₂ is closed Element of bool the carrier of T
(Cl c₂) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c<sub>2</sub>) is set
Cl ((Cl c<sub>2</sub>) `) is closed Element of bool the carrier of T
(Cl ((Cl c₂) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c₂) `)) is set
Cl ((Cl ((Cl c<sub>2</sub>) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c₂) `)) `)) is set
Cl ((Cl ((Cl ((Cl c₂) `)) `)) `) is closed Element of bool the carrier of T
Int ((Cl c<sub>2</sub>) `) is open Element of bool the carrier of T
Int (Cl ((Cl c₂) `)) is open Element of bool the carrier of T
Cl (Int (Cl ((Cl c<sub>2</sub>) `))) is closed Element of bool the carrier of T
Cl (Cl ((Cl c₂) `)) is closed Element of bool the carrier of T
T is 1-sorted
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
c<sub>2</sub> is Element of bool (bool the carrier of T)
P is Element of bool (bool the carrier of T)
c<sub>2</sub> \/ P is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
Cl c<sub>2</sub> is closed Element of bool the carrier of T
(Cl c<sub>2</sub>) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c₂) is set
Cl ((Cl c₂) `) is closed Element of bool the carrier of T
(Cl ((Cl c<sub>2</sub>) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c<sub>2</sub>) `)) is set
Cl ((Cl ((Cl c₂) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c₂) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) is set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} is non empty finite set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
(T,c₂) is set
Cl c₂ is closed Element of bool the carrier of T
(Cl c₂) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c<sub>2</sub>) is set
Cl ((Cl c<sub>2</sub>) `) is closed Element of bool the carrier of T
(Cl ((Cl c₂) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c₂) `)) is set
Cl ((Cl ((Cl c<sub>2</sub>) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c₂) `)) `)) is set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} is non empty finite set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
Cl c<sub>2</sub> is closed Element of bool the carrier of T
(Cl c<sub>2</sub>) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c₂) is set
Cl ((Cl c₂) `) is closed Element of bool the carrier of T
(Cl ((Cl c<sub>2</sub>) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c<sub>2</sub>) `)) is set
Cl ((Cl ((Cl c₂) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c₂) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) is set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} is non empty finite set
c₂ ` is Element of bool the carrier of T
the carrier of T \ c<sub>2</sub> is set
Cl (c<sub>2</sub> `) is closed Element of bool the carrier of T
(Cl (c₂ `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c₂ `)) is set
Cl ((Cl (c<sub>2</sub> `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c<sub>2</sub> `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c₂ `)) `)) is set
Cl ((Cl ((Cl (c₂ `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) is set
{(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} \/ {(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
bool (bool the carrier of T) is non empty set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
k2 is set
k3 is set
k3 is Element of bool (bool the carrier of T)
k2 is Element of bool (bool the carrier of T)
k3 \/ k2 is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c<sub>2</sub> is closed Element of bool the carrier of T
(Cl c<sub>2</sub>) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c₂) is set
Cl ((Cl c₂) `) is closed Element of bool the carrier of T
(Cl ((Cl c<sub>2</sub>) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c<sub>2</sub>) `)) is set
Cl ((Cl ((Cl c₂) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c₂) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) is set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} is non empty finite set
c₂ ` is Element of bool the carrier of T
the carrier of T \ c<sub>2</sub> is set
Cl (c<sub>2</sub> `) is closed Element of bool the carrier of T
(Cl (c₂ `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c₂ `)) is set
Cl ((Cl (c<sub>2</sub> `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c<sub>2</sub> `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c₂ `)) `)) is set
Cl ((Cl ((Cl (c₂ `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) is set
{(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} \/ {(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
(T,c<sub>2</sub>) is finite set
(T,(c<sub>2</sub> `)) is finite set
(T,c₂) \/ (T,(c₂ `)) is finite set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c<sub>2</sub> is closed Element of bool the carrier of T
(Cl c<sub>2</sub>) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c₂) is set
Cl ((Cl c₂) `) is closed Element of bool the carrier of T
(Cl ((Cl c<sub>2</sub>) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c<sub>2</sub>) `)) is set
Cl ((Cl ((Cl c₂) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c₂) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) is set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} is non empty finite set
c₂ ` is Element of bool the carrier of T
the carrier of T \ c<sub>2</sub> is set
Cl (c<sub>2</sub> `) is closed Element of bool the carrier of T
(Cl (c₂ `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c₂ `)) is set
Cl ((Cl (c<sub>2</sub> `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c<sub>2</sub> `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c₂ `)) `)) is set
Cl ((Cl ((Cl (c₂ `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) is set
{(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} \/ {(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
(T,c<sub>2</sub>) is finite set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
c<sub>2</sub> ` is Element of bool the carrier of T
the carrier of T \ c₂ is set
(T,c₂) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c₂ is closed Element of bool the carrier of T
(Cl c₂) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c<sub>2</sub>) is set
Cl ((Cl c<sub>2</sub>) `) is closed Element of bool the carrier of T
(Cl ((Cl c₂) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c₂) `)) is set
Cl ((Cl ((Cl c<sub>2</sub>) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c₂) `)) `)) is set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} is non empty finite set
Cl (c<sub>2</sub> `) is closed Element of bool the carrier of T
(Cl (c₂ `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c₂ `)) is set
Cl ((Cl (c<sub>2</sub> `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c<sub>2</sub> `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c₂ `)) `)) is set
Cl ((Cl ((Cl (c₂ `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) is set
{(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} \/ {(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
(T,(c<sub>2</sub> `)) is finite set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
Cl c₂ is closed Element of bool the carrier of T
(Cl c₂) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c<sub>2</sub>) is set
Cl ((Cl c<sub>2</sub>) `) is closed Element of bool the carrier of T
(Cl ((Cl c₂) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c₂) `)) is set
Cl ((Cl ((Cl c<sub>2</sub>) `)) `) is closed Element of bool the carrier of T
c<sub>2</sub> ` is Element of bool the carrier of T
the carrier of T \ c₂ is set
Cl (c₂ `) is closed Element of bool the carrier of T
(Cl (c<sub>2</sub> `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c<sub>2</sub> `)) is set
Cl ((Cl (c₂ `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c₂ `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c<sub>2</sub> `)) `)) is set
Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `) is closed Element of bool the carrier of T
{(Cl c₂),(Cl ((Cl c₂) `)),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),(Cl (c<sub>2</sub> `)),(Cl ((Cl (c₂ `)) `)),(Cl ((Cl ((Cl (c₂ `)) `)) `))} is non empty finite set
bool (bool the carrier of T) is non empty set
{(Cl (c<sub>2</sub> `)),(Cl ((Cl (c₂ `)) `)),(Cl ((Cl ((Cl (c₂ `)) `)) `))} is non empty finite set
{(Cl c<sub>2</sub>),(Cl ((Cl c<sub>2</sub>) `)),(Cl ((Cl ((Cl c₂) `)) `))} is non empty finite set
{(Cl c₂),(Cl ((Cl c₂) `)),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `))} \/ {(Cl (c<sub>2</sub> `)),(Cl ((Cl (c₂ `)) `)),(Cl ((Cl ((Cl (c₂ `)) `)) `))} is non empty finite set
(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c₂) `)) `)) is set
(Cl ((Cl ((Cl (c₂ `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c₂ `)) `)) `)) is set
{((Cl c<sub>2</sub>) `),((Cl ((Cl c₂) `)) `),((Cl ((Cl ((Cl c₂) `)) `)) `),((Cl (c<sub>2</sub> `)) `),((Cl ((Cl (c<sub>2</sub> `)) `)) `),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{((Cl (c₂ `)) `),((Cl ((Cl (c₂ `)) `)) `),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
{((Cl c<sub>2</sub>) `),((Cl ((Cl c₂) `)) `),((Cl ((Cl ((Cl c₂) `)) `)) `)} is non empty finite set
{((Cl c<sub>2</sub>) `),((Cl ((Cl c₂) `)) `),((Cl ((Cl ((Cl c₂) `)) `)) `)} \/ {((Cl (c<sub>2</sub> `)) `),((Cl ((Cl (c<sub>2</sub> `)) `)) `),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
(T,c₂) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c₂ is closed Element of bool the carrier of T
(Cl c₂) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c<sub>2</sub>) is set
Cl ((Cl c<sub>2</sub>) `) is closed Element of bool the carrier of T
(Cl ((Cl c₂) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c₂) `)) is set
Cl ((Cl ((Cl c<sub>2</sub>) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c₂) `)) `)) is set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} is non empty finite set
c<sub>2</sub> ` is Element of bool the carrier of T
the carrier of T \ c₂ is set
Cl (c₂ `) is closed Element of bool the carrier of T
(Cl (c<sub>2</sub> `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c<sub>2</sub> `)) is set
Cl ((Cl (c₂ `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c₂ `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c<sub>2</sub> `)) `)) is set
Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c₂ `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c₂ `)) `)) `)) is set
{(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} \/ {(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{(Cl c₂),(Cl ((Cl c₂) `)),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),(Cl (c<sub>2</sub> `)),(Cl ((Cl (c₂ `)) `)),(Cl ((Cl ((Cl (c₂ `)) `)) `))} is non empty finite set
{c<sub>2</sub>,(c<sub>2</sub> `)} is non empty finite set
{(Cl c₂),(Cl ((Cl c₂) `)),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),(Cl (c<sub>2</sub> `)),(Cl ((Cl (c₂ `)) `)),(Cl ((Cl ((Cl (c₂ `)) `)) `))} \/ {c<sub>2</sub>,(c<sub>2</sub> `)} is non empty finite set
{((Cl c₂) `),((Cl ((Cl c<sub>2</sub>) `)) `),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `),((Cl (c₂ `)) `),((Cl ((Cl (c₂ `)) `)) `),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
({(Cl c<sub>2</sub>),(Cl ((Cl c<sub>2</sub>) `)),(Cl ((Cl ((Cl c₂) `)) `)),(Cl (c₂ `)),(Cl ((Cl (c<sub>2</sub> `)) `)),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `))} \/ {c₂,(c₂ `)}) \/ {((Cl c<sub>2</sub>) `),((Cl ((Cl c₂) `)) `),((Cl ((Cl ((Cl c₂) `)) `)) `),((Cl (c<sub>2</sub> `)) `),((Cl ((Cl (c<sub>2</sub> `)) `)) `),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
k4 is set
k4 is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
(T,c₂) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c₂ is closed Element of bool the carrier of T
(Cl c₂) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c<sub>2</sub>) is set
Cl ((Cl c<sub>2</sub>) `) is closed Element of bool the carrier of T
(Cl ((Cl c₂) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c₂) `)) is set
Cl ((Cl ((Cl c<sub>2</sub>) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c₂) `)) `)) is set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} is non empty finite set
c<sub>2</sub> ` is Element of bool the carrier of T
the carrier of T \ c₂ is set
Cl (c₂ `) is closed Element of bool the carrier of T
(Cl (c<sub>2</sub> `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c<sub>2</sub> `)) is set
Cl ((Cl (c₂ `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c₂ `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c<sub>2</sub> `)) `)) is set
Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c₂ `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c₂ `)) `)) `)) is set
{(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} \/ {(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{c₂,(c₂ `)} is non empty finite set
(T,c<sub>2</sub>) is Element of bool (bool the carrier of T)
{(Cl c<sub>2</sub>),(Cl ((Cl c<sub>2</sub>) `)),(Cl ((Cl ((Cl c₂) `)) `)),(Cl (c₂ `)),(Cl ((Cl (c<sub>2</sub> `)) `)),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `))} is non empty finite set
{c₂,(c₂ `)} \/ (T,c<sub>2</sub>) is non empty set
(T,c<sub>2</sub>) is Element of bool (bool the carrier of T)
{((Cl c<sub>2</sub>) `),((Cl ((Cl c₂) `)) `),((Cl ((Cl ((Cl c₂) `)) `)) `),((Cl (c<sub>2</sub> `)) `),((Cl ((Cl (c<sub>2</sub> `)) `)) `),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
({c₂,(c₂ `)} \/ (T,c<sub>2</sub>)) \/ (T,c<sub>2</sub>) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c<sub>2</sub> is closed Element of bool the carrier of T
(Cl c<sub>2</sub>) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c₂) is set
Cl ((Cl c₂) `) is closed Element of bool the carrier of T
(Cl ((Cl c<sub>2</sub>) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c<sub>2</sub>) `)) is set
Cl ((Cl ((Cl c₂) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c₂) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) is set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} is non empty finite set
c₂ ` is Element of bool the carrier of T
the carrier of T \ c<sub>2</sub> is set
Cl (c<sub>2</sub> `) is closed Element of bool the carrier of T
(Cl (c₂ `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c₂ `)) is set
Cl ((Cl (c<sub>2</sub> `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c<sub>2</sub> `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c₂ `)) `)) is set
Cl ((Cl ((Cl (c₂ `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) is set
{(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} \/ {(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is finite Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c<sub>2</sub> is closed Element of bool the carrier of T
(Cl c<sub>2</sub>) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c₂) is set
Cl ((Cl c₂) `) is closed Element of bool the carrier of T
(Cl ((Cl c<sub>2</sub>) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c<sub>2</sub>) `)) is set
Cl ((Cl ((Cl c₂) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c₂) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) is set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} is non empty finite set
c₂ ` is Element of bool the carrier of T
the carrier of T \ c<sub>2</sub> is set
Cl (c<sub>2</sub> `) is closed Element of bool the carrier of T
(Cl (c₂ `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c₂ `)) is set
Cl ((Cl (c<sub>2</sub> `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c<sub>2</sub> `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c₂ `)) `)) is set
Cl ((Cl ((Cl (c₂ `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) is set
{(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} \/ {(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
P is Element of bool the carrier of T
P ` is Element of bool the carrier of T
the carrier of T \ P is set
Cl P is closed Element of bool the carrier of T
Cl ((Cl ((Cl ((Cl c₂) `)) `)) `) is closed Element of bool the carrier of T
14 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is finite Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c<sub>2</sub> is closed Element of bool the carrier of T
(Cl c<sub>2</sub>) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c₂) is set
Cl ((Cl c₂) `) is closed Element of bool the carrier of T
(Cl ((Cl c<sub>2</sub>) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c<sub>2</sub>) `)) is set
Cl ((Cl ((Cl c₂) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c₂) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) is set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} is non empty finite set
c₂ ` is Element of bool the carrier of T
the carrier of T \ c<sub>2</sub> is set
Cl (c<sub>2</sub> `) is closed Element of bool the carrier of T
(Cl (c₂ `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c₂ `)) is set
Cl ((Cl (c<sub>2</sub> `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c<sub>2</sub> `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c₂ `)) `)) is set
Cl ((Cl ((Cl (c₂ `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) is set
{(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} \/ {(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
card (T,c<sub>2</sub>) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
card {c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
card {(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
card ({c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} \/ {(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)}) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
(card {c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)}) + (card {(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)}) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
7 + 7 is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
Int c₂ is open Element of bool the carrier of T
Cl c₂ is closed Element of bool the carrier of T
Int (Cl c₂) is open Element of bool the carrier of T
Cl (Int c₂) is closed Element of bool the carrier of T
Cl (Int (Cl c₂)) is closed Element of bool the carrier of T
Int (Cl (Int c₂)) is open Element of bool the carrier of T
{c₂,(Int c₂),(Cl c₂),(Int (Cl c₂)),(Cl (Int c₂)),(Cl (Int (Cl c₂))),(Int (Cl (Int c₂)))} is non empty finite set
bool (bool the carrier of T) is non empty set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
x is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
(T,c₂) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Int c₂ is open Element of bool the carrier of T
Cl c₂ is closed Element of bool the carrier of T
Int (Cl c₂) is open Element of bool the carrier of T
Cl (Int c₂) is closed Element of bool the carrier of T
Cl (Int (Cl c₂)) is closed Element of bool the carrier of T
Int (Cl (Int c₂)) is open Element of bool the carrier of T
{c₂,(Int c₂),(Cl c₂),(Int (Cl c₂)),(Cl (Int c₂)),(Cl (Int (Cl c₂))),(Int (Cl (Int c₂)))} is non empty finite set
{c₂} is non empty finite set
{(Int c₂),(Int (Cl c₂)),(Int (Cl (Int c₂)))} is non empty finite set
{c₂} \/ {(Int c₂),(Int (Cl c₂)),(Int (Cl (Int c₂)))} is non empty finite set
{(Cl c₂),(Cl (Int c₂)),(Cl (Int (Cl c₂)))} is non empty finite set
({c₂} \/ {(Int c₂),(Int (Cl c₂)),(Int (Cl (Int c₂)))}) \/ {(Cl c₂),(Cl (Int c₂)),(Cl (Int (Cl c₂)))} is non empty finite set
{(Int c₂),(Cl c₂),(Int (Cl c₂)),(Cl (Int c₂)),(Cl (Int (Cl c₂))),(Int (Cl (Int c₂)))} is non empty finite set
{c₂} \/ {(Int c₂),(Cl c₂),(Int (Cl c₂)),(Cl (Int c₂)),(Cl (Int (Cl c₂))),(Int (Cl (Int c₂)))} is non empty finite set
{(Int c₂),(Int (Cl c₂)),(Int (Cl (Int c₂)))} \/ {(Cl c₂),(Cl (Int c₂)),(Cl (Int (Cl c₂)))} is non empty finite set
{c₂} \/ ({(Int c₂),(Int (Cl c₂)),(Int (Cl (Int c₂)))} \/ {(Cl c₂),(Cl (Int c₂)),(Cl (Int (Cl c₂)))}) is non empty finite set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
(T,c₂) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Int c₂ is open Element of bool the carrier of T
Cl c₂ is closed Element of bool the carrier of T
Int (Cl c₂) is open Element of bool the carrier of T
Cl (Int c₂) is closed Element of bool the carrier of T
Cl (Int (Cl c₂)) is closed Element of bool the carrier of T
Int (Cl (Int c₂)) is open Element of bool the carrier of T
{c₂,(Int c₂),(Cl c₂),(Int (Cl c₂)),(Cl (Int c₂)),(Cl (Int (Cl c₂))),(Int (Cl (Int c₂)))} is non empty finite set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
(T,c₂) is finite Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Int c₂ is open Element of bool the carrier of T
Cl c₂ is closed Element of bool the carrier of T
Int (Cl c₂) is open Element of bool the carrier of T
Cl (Int c₂) is closed Element of bool the carrier of T
Cl (Int (Cl c₂)) is closed Element of bool the carrier of T
Int (Cl (Int c₂)) is open Element of bool the carrier of T
{c₂,(Int c₂),(Cl c₂),(Int (Cl c₂)),(Cl (Int c₂)),(Cl (Int (Cl c₂))),(Int (Cl (Int c₂)))} is non empty finite set
P is Element of bool the carrier of T
Int P is open Element of bool the carrier of T
Cl P is closed Element of bool the carrier of T
Int (Cl (Int (Cl c₂))) is open Element of bool the carrier of T
{1} is non empty with_non-empty_elements non empty-membered finite V136() V137() V138() V139() V140() V141() Element of bool REAL
{1} \/ (RAT (2,4)) is non empty V136() V137() V138() Element of bool REAL
({1} \/ (RAT (2,4))) \/ ].4,5.[ is non empty V136() V137() V138() Element of bool REAL
(({1} \/ (RAT (2,4))) \/ ].4,5.[) \/ ].5,+infty.[ is non empty V136() V137() V138() Element of bool REAL
() is V136() V137() V138() Element of bool the carrier of R^1
Cl () is closed V136() V137() V138() Element of bool the carrier of R^1
[.2,+infty.[ is non empty V136() V137() V138() Element of bool REAL
{1} \/ [.2,+infty.[ is non empty V136() V137() V138() Element of bool REAL
{1} \/ (((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[) is non empty V136() V137() V138() Element of bool REAL
c₂ is V136() V137() V138() Element of bool the carrier of R^1
Cl c₂ is closed V136() V137() V138() Element of bool the carrier of R^1
P is V136() V137() V138() Element of bool the carrier of R^1
Cl P is closed V136() V137() V138() Element of bool the carrier of R^1
(Cl c₂) \/ (Cl P) is closed V136() V137() V138() Element of bool the carrier of R^1
(Cl ()) ` is open V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ (Cl ()) is V136() V137() V138() set
].1,2.[ is V136() V137() V138() Element of bool REAL
].-infty,1.[ \/ ].1,2.[ is non empty V136() V137() V138() Element of bool REAL
Cl ((Cl ()) `) is closed V136() V137() V138() Element of bool the carrier of R^1
(Cl ((Cl ()) `)) ` is open V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ (Cl ((Cl ()) `)) is V136() V137() V138() set
].2,+infty.[ is non empty V136() V137() V138() Element of bool REAL
Cl ((Cl ((Cl ()) `)) `) is closed V136() V137() V138() Element of bool the carrier of R^1
(Cl ((Cl ((Cl ()) `)) `)) ` is open V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ (Cl ((Cl ((Cl ()) `)) `)) is V136() V137() V138() set
].-infty,2.[ is non empty V136() V137() V138() Element of bool REAL
() ` is V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ () is V136() V137() V138() set
P is V136() V137() V138() Element of bool the carrier of R^1
P ` is V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ P is V136() V137() V138() set
{1} \/ (((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[) is non empty V136() V137() V138() Element of bool REAL
c₂ is V136() V137() V138() Element of bool the carrier of R^1
c₂ ` is V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ c<sub>2</sub> is V136() V137() V138() set
Cl (() `) is closed V136() V137() V138() Element of bool the carrier of R^1
].-infty,4.] is non empty V136() V137() V138() Element of bool REAL
].-infty,4.] \/ {5} is non empty V136() V137() V138() Element of bool REAL
(Cl (() `)) ` is open V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ (Cl (() `)) is V136() V137() V138() set
].4,5.[ \/ ].5,+infty.[ is non empty V136() V137() V138() Element of bool REAL
Cl ((Cl (() `)) `) is closed V136() V137() V138() Element of bool the carrier of R^1
[.4,+infty.[ is non empty V136() V137() V138() Element of bool REAL
(Cl ((Cl (() `)) `)) ` is open V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ (Cl ((Cl (() `)) `)) is V136() V137() V138() set
].-infty,4.[ is non empty V136() V137() V138() Element of bool REAL
Cl ((Cl ((Cl (() `)) `)) `) is closed V136() V137() V138() Element of bool the carrier of R^1
(Cl ((Cl ((Cl (() `)) `)) `)) ` is open V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ (Cl ((Cl ((Cl (() `)) `)) `)) is V136() V137() V138() set
].4,+infty.[ is non empty V136() V137() V138() Element of bool REAL
Int () is open V136() V137() V138() Element of bool the carrier of R^1
Cl (Int ()) is closed V136() V137() V138() Element of bool the carrier of R^1
Int (Cl (Int ())) is open V136() V137() V138() Element of bool the carrier of R^1
Int (Cl ()) is open V136() V137() V138() Element of bool the carrier of R^1
Cl (Int (Cl ())) is closed V136() V137() V138() Element of bool the carrier of R^1
3 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
3 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
3 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
{(Int ()),(Int (Cl ())),(Int (Cl (Int ())))} is non empty finite set
T is set
T is set
{(Cl ()),(Cl (Int ())),(Cl (Int (Cl ())))} is non empty finite set
T is set
0 is empty ext-real non positive non negative V16() finite V38() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() V142() Element of NAT
P is set
{(Int ()),(Int (Cl ())),(Int (Cl (Int ()))),(Cl ()),(Cl (Int ())),(Cl (Int (Cl ())))} is non empty finite set
{()} is non empty finite set
(R^1,()) is finite Element of bool (bool the carrier of R^1)
bool (bool the carrier of R^1) is non empty set
{(),(Int ()),(Cl ()),(Int (Cl ())),(Cl (Int ())),(Cl (Int (Cl ()))),(Int (Cl (Int ())))} is non empty finite set
card (R^1,()) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
(R^1,()) is Element of bool (bool the carrier of R^1)
{(Cl ()),(Cl ((Cl ()) `)),(Cl ((Cl ((Cl ()) `)) `)),(Cl (() `)),(Cl ((Cl (() `)) `)),(Cl ((Cl ((Cl (() `)) `)) `))} is non empty finite set
(R^1,()) is Element of bool (bool the carrier of R^1)
{((Cl ()) `),((Cl ((Cl ()) `)) `),((Cl ((Cl ((Cl ()) `)) `)) `),((Cl (() `)) `),((Cl ((Cl (() `)) `)) `),((Cl ((Cl ((Cl (() `)) `)) `)) `)} is non empty finite set
(R^1,()) is finite Element of bool (bool the carrier of R^1)
{(),(Cl ()),((Cl ()) `),(Cl ((Cl ()) `)),((Cl ((Cl ()) `)) `),(Cl ((Cl ((Cl ()) `)) `)),((Cl ((Cl ((Cl ()) `)) `)) `)} is non empty finite set
{(() `),(Cl (() `)),((Cl (() `)) `),(Cl ((Cl (() `)) `)),((Cl ((Cl (() `)) `)) `),(Cl ((Cl ((Cl (() `)) `)) `)),((Cl ((Cl ((Cl (() `)) `)) `)) `)} is non empty finite set
{(),(Cl ()),((Cl ()) `),(Cl ((Cl ()) `)),((Cl ((Cl ()) `)) `),(Cl ((Cl ((Cl ()) `)) `)),((Cl ((Cl ((Cl ()) `)) `)) `)} \/ {(() `),(Cl (() `)),((Cl (() `)) `),(Cl ((Cl (() `)) `)),((Cl ((Cl (() `)) `)) `),(Cl ((Cl ((Cl (() `)) `)) `)),((Cl ((Cl ((Cl (() `)) `)) `)) `)} is non empty finite set
{(),(() `)} is non empty finite set
T is Element of bool (bool the carrier of R^1)
[#] R^1 is non empty non proper open dense non boundary V136() V137() V138() Element of bool the carrier of R^1
[#] R^1 is non empty non proper open dense non boundary V136() V137() V138() Element of bool the carrier of R^1
T \/ (R^1,()) is Element of bool (bool the carrier of R^1)
(T \/ (R^1,())) \/ (R^1,()) is Element of bool (bool the carrier of R^1)
{} R^1 is empty proper finite V38() open boundary nowhere_dense V136() V137() V138() V139() V140() V141() V142() Element of bool the carrier of R^1
T is V136() V137() V138() Element of bool the carrier of R^1
T ` is V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ T is V136() V137() V138() set
T is with_non-empty_elements set
c₂ is set
{(),(() `)} is non empty finite set
{(),(() `)} \/ (R^1,()) is non empty set
({(),(() `)} \/ (R^1,())) \/ (R^1,()) is non empty set
{(),(() `)} is non empty finite set
{(),(() `)} \/ (R^1,()) is non empty set
({(),(() `)} \/ (R^1,())) \/ (R^1,()) is non empty set
T is with_non-empty_elements with_proper_subsets Element of bool (bool the carrier of R^1)
c₂ is with_non-empty_elements with_proper_subsets Element of bool (bool the carrier of R^1)
P is set
x is V136() V137() V138() Element of bool the carrier of R^1
T is V136() V137() V138() Element of bool the carrier of R^1
T is V136() V137() V138() Element of bool the carrier of R^1
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
(T,c₂) is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c₂ is closed Element of bool the carrier of T
(Cl c₂) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c<sub>2</sub>) is set
Cl ((Cl c<sub>2</sub>) `) is closed Element of bool the carrier of T
(Cl ((Cl c₂) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c₂) `)) is set
Cl ((Cl ((Cl c<sub>2</sub>) `)) `) is closed Element of bool the carrier of T
c<sub>2</sub> ` is Element of bool the carrier of T
the carrier of T \ c₂ is set
Cl (c₂ `) is closed Element of bool the carrier of T
(Cl (c<sub>2</sub> `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c<sub>2</sub> `)) is set
Cl ((Cl (c₂ `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c₂ `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c<sub>2</sub> `)) `)) is set
Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `) is closed Element of bool the carrier of T
{(Cl c₂),(Cl ((Cl c₂) `)),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),(Cl (c<sub>2</sub> `)),(Cl ((Cl (c₂ `)) `)),(Cl ((Cl ((Cl (c₂ `)) `)) `))} is non empty finite set
(T,c<sub>2</sub>) is Element of bool (bool the carrier of T)
(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c₂) `)) `)) is set
(Cl ((Cl ((Cl (c₂ `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c₂ `)) `)) `)) is set
{((Cl c<sub>2</sub>) `),((Cl ((Cl c₂) `)) `),((Cl ((Cl ((Cl c₂) `)) `)) `),((Cl (c<sub>2</sub> `)) `),((Cl ((Cl (c<sub>2</sub> `)) `)) `),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
card (R^1,()) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
card (R^1,()) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
(Cl (Int (Cl ()))) ` is open V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ (Cl (Int (Cl ()))) is V136() V137() V138() set
(Cl (Int ())) ` is open V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ (Cl (Int ())) is V136() V137() V138() set
{(),(() `)} is non empty finite set
c<sub>2</sub> is set
P is V136() V137() V138() Element of bool the carrier of R^1
P ` is V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ P is V136() V137() V138() set
c₂ is set
P is V136() V137() V138() Element of bool the carrier of R^1
P ` is V136() V137() V138() Element of bool the carrier of R^1
the carrier of R^1 \ P is V136() V137() V138() set
card (R^1,()) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
(R^1,()) \/ (R^1,()) is with_non-empty_elements finite Element of bool (bool the carrier of R^1)
card ((R^1,()) \/ (R^1,())) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
6 + 6 is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
12 is non empty ext-real positive non negative V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
{(),(() `)} \/ (R^1,()) is non empty finite set
({(),(() `)} \/ (R^1,())) \/ (R^1,()) is non empty finite set
card (({(),(() `)} \/ (R^1,())) \/ (R^1,())) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
{(),(() `)} \/ ((R^1,()) \/ (R^1,())) is non empty finite set
card ({(),(() `)} \/ ((R^1,()) \/ (R^1,()))) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
card {(),(() `)} is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
(card {(),(() `)}) + (card ((R^1,()) \/ (R^1,()))) is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
2 + 12 is ext-real V16() V51() V123() V134() V135() V136() V137() V138() V139() V140() V141() Element of NAT
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c₂ is Element of bool the carrier of T
(T,c₂) is finite Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Cl c₂ is closed Element of bool the carrier of T
(Cl c₂) ` is open Element of bool the carrier of T
the carrier of T \ (Cl c<sub>2</sub>) is set
Cl ((Cl c<sub>2</sub>) `) is closed Element of bool the carrier of T
(Cl ((Cl c₂) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl c₂) `)) is set
Cl ((Cl ((Cl c<sub>2</sub>) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl c₂) `)) `)) is set
{c₂,(Cl c₂),((Cl c₂) `),(Cl ((Cl c<sub>2</sub>) `)),((Cl ((Cl c₂) `)) `),(Cl ((Cl ((Cl c₂) `)) `)),((Cl ((Cl ((Cl c₂) `)) `)) `)} is non empty finite set
c<sub>2</sub> ` is Element of bool the carrier of T
the carrier of T \ c₂ is set
Cl (c₂ `) is closed Element of bool the carrier of T
(Cl (c<sub>2</sub> `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (c<sub>2</sub> `)) is set
Cl ((Cl (c₂ `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (c₂ `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (c<sub>2</sub> `)) `)) is set
Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (c₂ `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (c₂ `)) `)) `)) is set
{(c<sub>2</sub> `),(Cl (c₂ `)),((Cl (c<sub>2</sub> `)) `),(Cl ((Cl (c<sub>2</sub> `)) `)),((Cl ((Cl (c<sub>2</sub> `)) `)) `),(Cl ((Cl ((Cl (c₂ `)) `)) `)),((Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)) `)} is non empty finite set
{c<sub>2</sub>,(Cl c<sub>2</sub>),((Cl c<sub>2</sub>) `),(Cl ((Cl c₂) `)),((Cl ((Cl c<sub>2</sub>) `)) `),(Cl ((Cl ((Cl c<sub>2</sub>) `)) `)),((Cl ((Cl ((Cl c<sub>2</sub>) `)) `)) `)} \/ {(c₂ `),(Cl (c<sub>2</sub> `)),((Cl (c₂ `)) `),(Cl ((Cl (c₂ `)) `)),((Cl ((Cl (c₂ `)) `)) `),(Cl ((Cl ((Cl (c<sub>2</sub> `)) `)) `)),((Cl ((Cl ((Cl (c₂ `)) `)) `)) `)} is non empty finite set
P is Element of bool the carrier of T
Cl P is closed Element of bool the carrier of T
P is Element of bool the carrier of T
P ` is Element of bool the carrier of T
the carrier of T \ P is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
c<sub>2</sub> is Element of bool the carrier of T
(T,c<sub>2</sub>) is finite Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Int c<sub>2</sub> is open Element of bool the carrier of T
Cl c<sub>2</sub> is closed Element of bool the carrier of T
Int (Cl c<sub>2</sub>) is open Element of bool the carrier of T
Cl (Int c<sub>2</sub>) is closed Element of bool the carrier of T
Cl (Int (Cl c<sub>2</sub>)) is closed Element of bool the carrier of T
Int (Cl (Int c<sub>2</sub>)) is open Element of bool the carrier of T
{c<sub>2</sub>,(Int c<sub>2</sub>),(Cl c<sub>2</sub>),(Int (Cl c<sub>2</sub>)),(Cl (Int c<sub>2</sub>)),(Cl (Int (Cl c<sub>2</sub>))),(Int (Cl (Int c<sub>2</sub>)))} is non empty finite set
P is Element of bool the carrier of T
Int P is open Element of bool the carrier of T
P is Element of bool the carrier of T
Cl P is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{} T is empty proper finite V38() open boundary nowhere_dense V136() V137() V138() V139() V140() V141() V142() Element of bool the carrier of T
(T,({} T)) is non empty finite (T) (T) Element of bool (bool the carrier of T)
Int ({} T) is empty proper finite V38() open boundary nowhere_dense V136() V137() V138() V139() V140() V141() V142() Element of bool the carrier of T
Cl ({} T) is closed Element of bool the carrier of T
Int (Cl ({} T)) is open Element of bool the carrier of T
Cl (Int ({} T)) is closed Element of bool the carrier of T
Cl (Int (Cl ({} T))) is closed Element of bool the carrier of T
Int (Cl (Int ({} T))) is open Element of bool the carrier of T
{({} T),(Int ({} T)),(Cl ({} T)),(Int (Cl ({} T))),(Cl (Int ({} T))),(Cl (Int (Cl ({} T)))),(Int (Cl (Int ({} T))))} is non empty finite set
{} T is empty proper finite V38() open boundary nowhere_dense V136() V137() V138() V139() V140() V141() V142() Element of bool the carrier of T
(T,({} T)) is non empty finite compl-closed (T) Element of bool (bool the carrier of T)
Cl ({} T) is closed Element of bool the carrier of T
(Cl ({} T)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ({} T)) is set
Cl ((Cl ({} T)) `) is closed Element of bool the carrier of T
(Cl ((Cl ({} T)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ({} T)) `)) is set
Cl ((Cl ((Cl ({} T)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl ({} T)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl ({} T)) `)) `)) is set
{({} T),(Cl ({} T)),((Cl ({} T)) `),(Cl ((Cl ({} T)) `)),((Cl ((Cl ({} T)) `)) `),(Cl ((Cl ((Cl ({} T)) `)) `)),((Cl ((Cl ((Cl ({} T)) `)) `)) `)} is non empty finite set
({} T) ` is closed dense Element of bool the carrier of T
the carrier of T \ ({} T) is set
Cl (({} T) `) is closed Element of bool the carrier of T
(Cl (({} T) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl (({} T) `)) is set
Cl ((Cl (({} T) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl (({} T) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl (({} T) `)) `)) is set
Cl ((Cl ((Cl (({} T) `)) `)) `) is closed Element of bool the carrier of T
(Cl ((Cl ((Cl (({} T) `)) `)) `)) ` is open Element of bool the carrier of T
the carrier of T \ (Cl ((Cl ((Cl (({} T) `)) `)) `)) is set
{(({} T) `),(Cl (({} T) `)),((Cl (({} T) `)) `),(Cl ((Cl (({} T) `)) `)),((Cl ((Cl (({} T) `)) `)) `),(Cl ((Cl ((Cl (({} T) `)) `)) `)),((Cl ((Cl ((Cl (({} T) `)) `)) `)) `)} is non empty finite set
{({} T),(Cl ({} T)),((Cl ({} T)) `),(Cl ((Cl ({} T)) `)),((Cl ((Cl ({} T)) `)) `),(Cl ((Cl ((Cl ({} T)) `)) `)),((Cl ((Cl ((Cl ({} T)) `)) `)) `)} \/ {(({} T) `),(Cl (({} T) `)),((Cl (({} T) `)) `),(Cl ((Cl (({} T) `)) `)),((Cl ((Cl (({} T) `)) `)) `),(Cl ((Cl ((Cl (({} T) `)) `)) `)),((Cl ((Cl ((Cl (({} T) `)) `)) `)) `)} is non empty finite set