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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

Cl ((Cl ((Cl ((Cl c

Int ((Cl c

Int (Cl ((Cl c

Cl (Int (Cl ((Cl c

Cl (Cl ((Cl c

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

P is Element of bool (bool the carrier of T)

c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

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

(T,c

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{(c

{c

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

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{(c

{c

(T,c

(T,(c

(T,c

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

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{(c

{c

(T,c

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

c

the carrier of T \ c

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{(c

{c

(T,(c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

{(Cl c

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

{(Cl (c

{(Cl c

{(Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{((Cl c

{((Cl (c

{((Cl c

{((Cl c

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

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{(c

{c

{(Cl c

{c

{(Cl c

{((Cl c

({(Cl c

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

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{(c

{c

{c

(T,c

{(Cl c

{c

(T,c

{((Cl c

({c

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

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{(c

{c

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

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{(c

{c

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

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

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

{c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{(c

{c

card (T,c

card {c

card {(c

card ({c

(card {c

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

Int c

Cl c

Int (Cl c

Cl (Int c

Cl (Int (Cl c

Int (Cl (Int c

{c

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

(T,c

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

Int c

Cl c

Int (Cl c

Cl (Int c

Cl (Int (Cl c

Int (Cl (Int c

{c

{c

{(Int c

{c

{(Cl c

({c

{(Int c

{c

{(Int c

{c

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

(T,c

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

Int c

Cl c

Int (Cl c

Cl (Int c

Cl (Int (Cl c

Int (Cl (Int c

{c

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

(T,c

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

Int c

Cl c

Int (Cl c

Cl (Int c

Cl (Int (Cl c

Int (Cl (Int c

{c

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

{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

Cl c

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

c

the carrier of R^1 \ c

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

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

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

c

the carrier of T \ c

Cl (c

(Cl (c

the carrier of T \ (Cl (c

Cl ((Cl (c

(Cl ((Cl (c

the carrier of T \ (Cl ((Cl (c

Cl ((Cl ((Cl (c

{(Cl c

(T,c

(Cl ((Cl ((Cl c

the carrier of T \ (Cl ((Cl ((Cl c

(Cl ((Cl ((Cl (c

the carrier of T \ (Cl ((Cl ((Cl (c

{((Cl c

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

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

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

(T,c

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

Cl c

(Cl c

the carrier of T \ (Cl c

Cl ((Cl c

(Cl ((Cl c

the carrier of T \ (Cl ((Cl c

Cl ((Cl ((Cl c

(Cl ((Cl ((Cl c

the carrier of T