:: TEX_1 semantic presentation

K142() is set

K146() is non empty V24() V25() V26() V31() cardinal limit_cardinal Element of K10(K142())

K10(K142()) is non empty set

K121() is non empty V24() V25() V26() V31() cardinal limit_cardinal set

K10(K121()) is non empty V31() set

1 is non empty V24() V25() V26() V30() V31() cardinal Element of K146()

K11(1,1) is non empty set

K10(K11(1,1)) is non empty set

K11(K11(1,1),1) is non empty set

K10(K11(K11(1,1),1)) is non empty set

K11(K11(1,1),K142()) is set

K10(K11(K11(1,1),K142())) is non empty set

K11(K142(),K142()) is set

K11(K11(K142(),K142()),K142()) is set

K10(K11(K11(K142(),K142()),K142())) is non empty set

2 is non empty V24() V25() V26() V30() V31() cardinal Element of K146()

K11(2,2) is non empty set

K11(K11(2,2),K142()) is set

K10(K11(K11(2,2),K142())) is non empty set

{} is empty V24() V25() V26() V28() V29() V30() V31() cardinal {} -element set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

X modified_with_respect_to A is non empty strict TopSpace-like TopStruct

the carrier of (X modified_with_respect_to A) is non empty set

K10( the carrier of (X modified_with_respect_to A)) is non empty set

Z is Element of K10( the carrier of X)

C is Element of K10( the carrier of (X modified_with_respect_to A))

the topology of X is non empty Element of K10(K10( the carrier of X))

K10(K10( the carrier of X)) is non empty set

A -extension_of_the_topology_of X is Element of K10(K10( the carrier of X))

the topology of (X modified_with_respect_to A) is non empty Element of K10(K10( the carrier of (X modified_with_respect_to A)))

K10(K10( the carrier of (X modified_with_respect_to A))) is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

X modified_with_respect_to A is non empty strict TopSpace-like TopStruct

the carrier of (X modified_with_respect_to A) is non empty set

K10( the carrier of (X modified_with_respect_to A)) is non empty set

Z is Element of K10( the carrier of X)

C is Element of K10( the carrier of (X modified_with_respect_to A))

C ` is Element of K10( the carrier of (X modified_with_respect_to A))

the carrier of (X modified_with_respect_to A) \ C is set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

X modified_with_respect_to (A `) is non empty strict TopSpace-like TopStruct

the carrier of (X modified_with_respect_to (A `)) is non empty set

K10( the carrier of (X modified_with_respect_to (A `))) is non empty set

Z is Element of K10( the carrier of (X modified_with_respect_to (A `)))

Z ` is Element of K10( the carrier of (X modified_with_respect_to (A `)))

the carrier of (X modified_with_respect_to (A `)) \ Z is set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

X modified_with_respect_to A is non empty strict TopSpace-like TopStruct

the carrier of (X modified_with_respect_to A) is non empty set

K10( the carrier of (X modified_with_respect_to A)) is non empty set

Z is Element of K10( the carrier of (X modified_with_respect_to A))

Cl Z is closed Element of K10( the carrier of (X modified_with_respect_to A))

(Cl Z) ` is open Element of K10( the carrier of (X modified_with_respect_to A))

the carrier of (X modified_with_respect_to A) \ (Cl Z) is set

the topology of (X modified_with_respect_to A) is non empty Element of K10(K10( the carrier of (X modified_with_respect_to A)))

K10(K10( the carrier of (X modified_with_respect_to A))) is non empty set

A -extension_of_the_topology_of X is Element of K10(K10( the carrier of X))

K10(K10( the carrier of X)) is non empty set

the topology of X is non empty Element of K10(K10( the carrier of X))

{ (b

Y1 is Element of K10( the carrier of X)

A1 is Element of K10( the carrier of X)

A1 /\ A is Element of K10( the carrier of X)

Y1 \/ (A1 /\ A) is Element of K10( the carrier of X)

(A1 /\ A) /\ ((Cl Z) `) is Element of K10( the carrier of (X modified_with_respect_to A))

(Y1 \/ (A1 /\ A)) /\ ((Cl Z) `) is Element of K10( the carrier of (X modified_with_respect_to A))

Y1 /\ ((Cl Z) `) is Element of K10( the carrier of (X modified_with_respect_to A))

(Y1 /\ ((Cl Z) `)) \/ {} is set

C is Element of K10( the carrier of X)

Cl A is closed Element of K10( the carrier of X)

(Cl A) /\ C is Element of K10( the carrier of X)

[#] X is non empty non proper open closed dense non boundary Element of K10( the carrier of X)

[#] (X modified_with_respect_to A) is non empty non proper open closed dense non boundary Element of K10( the carrier of (X modified_with_respect_to A))

{} (X modified_with_respect_to A) is empty proper V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense Element of K10( the carrier of (X modified_with_respect_to A))

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

X modified_with_respect_to A is non empty strict TopSpace-like TopStruct

the carrier of (X modified_with_respect_to A) is non empty set

K10( the carrier of (X modified_with_respect_to A)) is non empty set

Z is Element of K10( the carrier of (X modified_with_respect_to A))

C is Element of K10( the carrier of (X modified_with_respect_to A))

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

X modified_with_respect_to (A `) is non empty strict TopSpace-like TopStruct

the carrier of (X modified_with_respect_to (A `)) is non empty set

K10( the carrier of (X modified_with_respect_to (A `))) is non empty set

Z is Element of K10( the carrier of (X modified_with_respect_to (A `)))

Z ` is Element of K10( the carrier of (X modified_with_respect_to (A `)))

the carrier of (X modified_with_respect_to (A `)) \ Z is set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

X modified_with_respect_to (A `) is non empty strict TopSpace-like TopStruct

the carrier of (X modified_with_respect_to (A `)) is non empty set

K10( the carrier of (X modified_with_respect_to (A `))) is non empty set

Z is Element of K10( the carrier of (X modified_with_respect_to (A `)))

C is Element of K10( the carrier of (X modified_with_respect_to (A `)))

X is set

A is set

K10(A) is non empty set

Z is set

C is set

K10(C) is non empty set

X is non empty 1-sorted

the carrier of X is non empty set

K10( the carrier of X) is non empty set

the Element of the carrier of X is Element of the carrier of X

{ the Element of the carrier of X} is non empty trivial 1 -element Element of K10( the carrier of X)

C is Element of the carrier of X

A is Element of K10( the carrier of X)

C is Element of K10( the carrier of X)

A is Element of the carrier of X

{A} is non empty trivial 1 -element Element of K10( the carrier of X)

K10( the carrier of X) is non empty set

Z is Element of the carrier of X

C is Element of the carrier of X

the non empty trivial V46() 1 -element 1-sorted is non empty trivial V46() 1 -element 1-sorted

the carrier of the non empty trivial V46() 1 -element 1-sorted is non empty trivial V31() 1 -element set

K10( the carrier of the non empty trivial V46() 1 -element 1-sorted ) is non empty set

K10(K10( the carrier of the non empty trivial V46() 1 -element 1-sorted )) is non empty set

A is Element of K10(K10( the carrier of the non empty trivial V46() 1 -element 1-sorted ))

Z is Element of K10(K10( the carrier of the non empty trivial V46() 1 -element 1-sorted ))

TopStruct(# the carrier of the non empty trivial V46() 1 -element 1-sorted ,Z #) is non empty strict TopStruct

the carrier of TopStruct(# the carrier of the non empty trivial V46() 1 -element 1-sorted ,Z #) is non empty set

the non empty non trivial 1-sorted is non empty non trivial 1-sorted

the carrier of the non empty non trivial 1-sorted is non empty non trivial set

K10( the carrier of the non empty non trivial 1-sorted ) is non empty set

K10(K10( the carrier of the non empty non trivial 1-sorted )) is non empty set

A is Element of K10(K10( the carrier of the non empty non trivial 1-sorted ))

TopStruct(# the carrier of the non empty non trivial 1-sorted ,A #) is non empty strict TopStruct

X is non empty trivial V46() 1 -element TopStruct

the topology of X is Element of K10(K10( the carrier of X))

the carrier of X is non empty trivial V31() 1 -element set

K10( the carrier of X) is non empty set

K10(K10( the carrier of X)) is non empty set

A is Element of the carrier of X

{A} is non empty trivial 1 -element Element of K10( the carrier of X)

C is trivial Element of K10( the carrier of X)

Z is trivial Element of K10( the carrier of X)

bool Z is non empty Element of K10(K10(Z))

K10(Z) is non empty set

K10(K10(Z)) is non empty set

{{},Z} is non empty set

Z \ C is trivial Element of K10( the carrier of X)

Z \ C is trivial Element of K10( the carrier of X)

{{}, the carrier of X} is non empty set

C is TopSpace-like anti-discrete almost_discrete TopStruct

the non empty trivial V46() 1 -element 1-sorted is non empty trivial V46() 1 -element 1-sorted

the carrier of the non empty trivial V46() 1 -element 1-sorted is non empty trivial V31() 1 -element set

K10( the carrier of the non empty trivial V46() 1 -element 1-sorted ) is non empty set

K10(K10( the carrier of the non empty trivial V46() 1 -element 1-sorted )) is non empty set

bool the carrier of the non empty trivial V46() 1 -element 1-sorted is non empty Element of K10(K10( the carrier of the non empty trivial V46() 1 -element 1-sorted ))

A is Element of K10(K10( the carrier of the non empty trivial V46() 1 -element 1-sorted ))

TopStruct(# the carrier of the non empty trivial V46() 1 -element 1-sorted ,A #) is non empty strict TopStruct

C is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

C is non empty TopSpace-like TopStruct

the carrier of C is non empty set

X is non empty trivial V46() 1 -element TopSpace-like TopStruct

the carrier of X is non empty trivial V31() 1 -element set

the topology of X is non empty Element of K10(K10( the carrier of X))

K10( the carrier of X) is non empty set

K10(K10( the carrier of X)) is non empty set

bool the carrier of X is non empty Element of K10(K10( the carrier of X))

{{}, the carrier of X} is non empty set

A is Element of the carrier of X

{A} is non empty trivial 1 -element Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

bool the carrier of X is non empty Element of K10(K10( the carrier of X))

K10( the carrier of X) is non empty set

K10(K10( the carrier of X)) is non empty set

{{}, the carrier of X} is non empty set

the Element of the carrier of X is Element of the carrier of X

Z is Element of the carrier of X

{Z} is non empty trivial 1 -element Element of K10( the carrier of X)

A is Element of the carrier of X

{A} is non empty trivial 1 -element Element of K10( the carrier of X)

{{},1} is non empty set

K10({{},1}) is non empty set

K10(K10({{},1})) is non empty set

bool {{},1} is non empty Element of K10(K10({{},1}))

A is Element of K10(K10({{},1}))

Z is Element of K10(K10({{},1}))

TopStruct(# {{},1},Z #) is non empty strict TopStruct

C is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of C is non empty set

C is Element of the carrier of C

{C} is non empty trivial 1 -element Element of K10( the carrier of C)

K10( the carrier of C) is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

X is set

{{},X} is non empty set

K10(X) is non empty set

K10(K10(X)) is non empty set

bool X is non empty Element of K10(K10(X))

X is set

(X) is Element of K10(K10(X))

K10(X) is non empty set

K10(K10(X)) is non empty set

{{},X} is non empty set

X is set

(X) is non empty Element of K10(K10(X))

K10(X) is non empty set

K10(K10(X)) is non empty set

{{},X} is non empty set

TopStruct(# X,(X) #) is strict TopStruct

X is set

(X) is TopStruct

(X) is non empty Element of K10(K10(X))

K10(X) is non empty set

K10(K10(X)) is non empty set

{{},X} is non empty set

TopStruct(# X,(X) #) is strict TopStruct

Z is TopSpace-like anti-discrete almost_discrete TopStruct

X is non empty set

(X) is strict TopSpace-like anti-discrete almost_discrete TopStruct

(X) is non empty Element of K10(K10(X))

K10(X) is non empty set

K10(K10(X)) is non empty set

{{},X} is non empty set

TopStruct(# X,(X) #) is non empty strict TopStruct

X is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Cl A is closed Element of K10( the carrier of X)

X is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Int A is open Element of K10( the carrier of X)

[#] X is non empty non proper open closed dense non boundary Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Cl A is closed Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Int A is open Element of K10( the carrier of X)

X is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Cl A is closed Element of K10( the carrier of X)

Int A is open Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Z is Element of K10( the carrier of X)

Cl A is closed Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Z is Element of K10( the carrier of X)

Int A is open Element of K10( the carrier of X)

X is set

1TopSp X is TopStruct

bool X is non empty Element of K10(K10(X))

K10(X) is non empty set

K10(K10(X)) is non empty set

[#] (bool X) is non empty non proper Element of K10((bool X))

K10((bool X)) is non empty set

TopStruct(# X,([#] (bool X)) #) is strict TopStruct

X is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Cl A is closed Element of K10( the carrier of X)

Int A is open Element of K10( the carrier of X)

Z is Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Cl A is closed Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

Int A is open Element of K10( the carrier of X)

X is non empty set

(X) is non empty strict TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

(X) is non empty Element of K10(K10(X))

K10(X) is non empty set

K10(K10(X)) is non empty set

{{},X} is non empty set

TopStruct(# X,(X) #) is non empty strict TopStruct

1TopSp X is TopSpace-like discrete almost_discrete TopStruct

bool X is non empty Element of K10(K10(X))

[#] (bool X) is non empty non proper Element of K10((bool X))

K10((bool X)) is non empty set

TopStruct(# X,([#] (bool X)) #) is non empty strict TopStruct

the Element of X is Element of X

{ the Element of X} is non empty trivial 1 -element Element of K10(X)

A is Element of X

{A} is non empty trivial 1 -element Element of K10(X)

{{},1} is non empty set

1TopSp {{},1} is TopSpace-like discrete almost_discrete TopStruct

bool {{},1} is non empty Element of K10(K10({{},1}))

K10({{},1}) is non empty set

K10(K10({{},1})) is non empty set

[#] (bool {{},1}) is non empty non proper Element of K10((bool {{},1}))

K10((bool {{},1})) is non empty set

TopStruct(# {{},1},([#] (bool {{},1})) #) is non empty strict TopStruct

the carrier of (1TopSp {{},1}) is set

the topology of (1TopSp {{},1}) is non empty Element of K10(K10( the carrier of (1TopSp {{},1})))

K10( the carrier of (1TopSp {{},1})) is non empty set

K10(K10( the carrier of (1TopSp {{},1}))) is non empty set

TopStruct(# the carrier of (1TopSp {{},1}), the topology of (1TopSp {{},1}) #) is strict TopSpace-like TopStruct

({{},1}) is non empty strict TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

({{},1}) is non empty Element of K10(K10({{},1}))

{{},{{},1}} is non empty set

TopStruct(# {{},1},({{},1}) #) is non empty strict TopStruct

the carrier of ({{},1}) is non empty set

the topology of ({{},1}) is non empty Element of K10(K10( the carrier of ({{},1})))

K10( the carrier of ({{},1})) is non empty set

K10(K10( the carrier of ({{},1}))) is non empty set

TopStruct(# the carrier of ({{},1}), the topology of ({{},1}) #) is non empty strict TopSpace-like TopStruct

Z is Element of {{},1}

{Z} is non empty trivial 1 -element Element of K10({{},1})

{{},1} is non empty set

({{},1}) is non empty strict TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

({{},1}) is non empty Element of K10(K10({{},1}))

K10({{},1}) is non empty set

K10(K10({{},1})) is non empty set

{{},{{},1}} is non empty set

TopStruct(# {{},1},({{},1}) #) is non empty strict TopStruct

the carrier of ({{},1}) is non empty set

the topology of ({{},1}) is non empty Element of K10(K10( the carrier of ({{},1})))

K10( the carrier of ({{},1})) is non empty set

K10(K10( the carrier of ({{},1}))) is non empty set

TopStruct(# the carrier of ({{},1}), the topology of ({{},1}) #) is non empty strict TopSpace-like TopStruct

1TopSp {{},1} is TopSpace-like discrete almost_discrete TopStruct

bool {{},1} is non empty Element of K10(K10({{},1}))

[#] (bool {{},1}) is non empty non proper Element of K10((bool {{},1}))

K10((bool {{},1})) is non empty set

TopStruct(# {{},1},([#] (bool {{},1})) #) is non empty strict TopStruct

the carrier of (1TopSp {{},1}) is set

the topology of (1TopSp {{},1}) is non empty Element of K10(K10( the carrier of (1TopSp {{},1})))

K10( the carrier of (1TopSp {{},1})) is non empty set

K10(K10( the carrier of (1TopSp {{},1}))) is non empty set

TopStruct(# the carrier of (1TopSp {{},1}), the topology of (1TopSp {{},1}) #) is strict TopSpace-like TopStruct

Z is Element of {{},1}

{Z} is non empty trivial 1 -element Element of K10({{},1})

X is set

K10(X) is non empty set

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

A is Element of X

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

X is set

A is Element of X

(X,A) is TopStruct

K10(X) is non empty set

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

Z is Element of K10(X)

A1 is Element of K10(X)

the carrier of TopStruct(# X,((bool X) \ { b

K10( the carrier of TopStruct(# X,((bool X) \ { b

K10(K10( the carrier of TopStruct(# X,((bool X) \ { b

A1 is Element of K10(K10( the carrier of TopStruct(# X,((bool X) \ { b

the topology of TopStruct(# X,((bool X) \ { b

A1 /\ { b

union A1 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

union A1 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

Y2 is Element of K10(X)

Y2 is set

A2 is Element of K10(X)

Y2 is set

Y2 is Element of K10(X)

union A1 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

union A1 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

A1 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

A2 is Element of K10(X)

A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

A2 is Element of K10(X)

A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

A2 is Element of K10(X)

A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of TopStruct(# X,((bool X) \ { b

K10( the carrier of TopStruct(# X,((bool X) \ { b

X is non empty set

A is Element of X

(X,A) is strict TopSpace-like TopStruct

K10(X) is non empty set

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

X is non empty set

A is Element of X

(X,A) is non empty strict TopSpace-like TopStruct

K10(X) is non empty set

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

K10( the carrier of (X,A)) is non empty set

{A} is non empty trivial 1 -element Element of K10(X)

Z is Element of K10( the carrier of (X,A))

Z ` is Element of K10( the carrier of (X,A))

the carrier of (X,A) \ Z is set

Y1 is Element of K10(X)

the topology of (X,A) is non empty Element of K10(K10( the carrier of (X,A)))

K10(K10( the carrier of (X,A))) is non empty set

the topology of (X,A) is non empty Element of K10(K10( the carrier of (X,A)))

K10(K10( the carrier of (X,A))) is non empty set

X is non empty set

A is Element of X

{A} is non empty trivial 1 -element Element of K10(X)

K10(X) is non empty set

X \ {A} is Element of K10(X)

(X,A) is non empty strict TopSpace-like TopStruct

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

K10( the carrier of (X,A)) is non empty set

C is Element of K10( the carrier of (X,A))

Int C is open Element of K10( the carrier of (X,A))

the topology of (X,A) is non empty Element of K10(K10( the carrier of (X,A)))

K10(K10( the carrier of (X,A))) is non empty set

C \ {A} is Element of K10( the carrier of (X,A))

Y1 is Element of K10( the carrier of (X,A))

A1 is Element of K10(X)

X is non empty set

A is Element of X

(X,A) is non empty strict TopSpace-like TopStruct

K10(X) is non empty set

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

K10( the carrier of (X,A)) is non empty set

{A} is non empty trivial 1 -element Element of K10(X)

X \ {A} is Element of K10(X)

Z is Element of K10( the carrier of (X,A))

Z ` is Element of K10( the carrier of (X,A))

the carrier of (X,A) \ Z is set

[#] (X,A) is non empty non proper open closed dense non boundary Element of K10( the carrier of (X,A))

([#] (X,A)) \ (X \ {A}) is Element of K10( the carrier of (X,A))

([#] (X,A)) \ Z is Element of K10( the carrier of (X,A))

C is Element of K10( the carrier of (X,A))

{} (X,A) is empty proper V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense Element of K10( the carrier of (X,A))

(Z `) ` is Element of K10( the carrier of (X,A))

the carrier of (X,A) \ (Z `) is set

C is Element of K10( the carrier of (X,A))

C ` is Element of K10( the carrier of (X,A))

the carrier of (X,A) \ C is set

X is non empty set

A is Element of X

{A} is non empty trivial 1 -element Element of K10(X)

K10(X) is non empty set

X \ {A} is Element of K10(X)

(X,A) is non empty strict TopSpace-like TopStruct

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

K10( the carrier of (X,A)) is non empty set

C is Element of K10( the carrier of (X,A))

C ` is Element of K10( the carrier of (X,A))

the carrier of (X,A) \ C is set

[#] (X,A) is non empty non proper open closed dense non boundary Element of K10( the carrier of (X,A))

Z is Element of K10( the carrier of (X,A))

([#] (X,A)) \ Z is Element of K10( the carrier of (X,A))

([#] (X,A)) \ (([#] (X,A)) \ Z) is Element of K10( the carrier of (X,A))

{} (X,A) is empty proper V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense Element of K10( the carrier of (X,A))

Z is Element of K10( the carrier of (X,A))

Z ` is Element of K10( the carrier of (X,A))

the carrier of (X,A) \ Z is set

{{},1} is non empty set

A is Element of {{},1}

({{},1},A) is non empty strict TopSpace-like TopStruct

K10({{},1}) is non empty set

bool {{},1} is non empty Element of K10(K10({{},1}))

K10(K10({{},1})) is non empty set

{ b

(bool {{},1}) \ { b

TopStruct(# {{},1},((bool {{},1}) \ { b

the carrier of ({{},1},A) is non empty set

K10( the carrier of ({{},1},A)) is non empty set

{A} is non empty trivial 1 -element Element of K10({{},1})

C is non empty Element of K10( the carrier of ({{},1},A))

{{},1} \ C is Element of K10({{},1})

Int C is open Element of K10( the carrier of ({{},1},A))

X is non empty set

A is Element of X

(X,A) is non empty strict TopSpace-like TopStruct

K10(X) is non empty set

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

the topology of (X,A) is non empty Element of K10(K10( the carrier of (X,A)))

K10( the carrier of (X,A)) is non empty set

K10(K10( the carrier of (X,A))) is non empty set

TopStruct(# the carrier of (X,A), the topology of (X,A) #) is non empty strict TopSpace-like TopStruct

{A} is non empty trivial 1 -element Element of K10(X)

Z is non empty TopSpace-like TopStruct

the carrier of Z is non empty set

the topology of Z is non empty Element of K10(K10( the carrier of Z))

K10( the carrier of Z) is non empty set

K10(K10( the carrier of Z)) is non empty set

TopStruct(# the carrier of Z, the topology of Z #) is non empty strict TopSpace-like TopStruct

C is Element of K10( the carrier of Z)

C is Element of K10( the carrier of (X,A))

C is Element of K10( the carrier of (X,A))

C is Element of K10( the carrier of Z)

C is Element of K10( the carrier of Z)

C is Element of K10( the carrier of Z)

C is Element of K10( the carrier of (X,A))

X is non empty set

A is Element of X

(X,A) is non empty strict TopSpace-like TopStruct

K10(X) is non empty set

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

the topology of (X,A) is non empty Element of K10(K10( the carrier of (X,A)))

K10( the carrier of (X,A)) is non empty set

K10(K10( the carrier of (X,A))) is non empty set

TopStruct(# the carrier of (X,A), the topology of (X,A) #) is non empty strict TopSpace-like TopStruct

{A} is non empty trivial 1 -element Element of K10(X)

X \ {A} is Element of K10(X)

Z is non empty TopSpace-like TopStruct

the carrier of Z is non empty set

the topology of Z is non empty Element of K10(K10( the carrier of Z))

K10( the carrier of Z) is non empty set

K10(K10( the carrier of Z)) is non empty set

TopStruct(# the carrier of Z, the topology of Z #) is non empty strict TopSpace-like TopStruct

C is Element of K10( the carrier of Z)

C is Element of K10( the carrier of (X,A))

C is Element of K10( the carrier of (X,A))

C is Element of K10( the carrier of Z)

C is Element of K10( the carrier of (X,A))

[#] (X,A) is non empty non proper open closed dense non boundary Element of K10( the carrier of (X,A))

[#] Z is non empty non proper open closed dense non boundary Element of K10( the carrier of Z)

X is non empty set

A is Element of X

(X,A) is non empty strict TopSpace-like TopStruct

K10(X) is non empty set

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

the topology of (X,A) is non empty Element of K10(K10( the carrier of (X,A)))

K10( the carrier of (X,A)) is non empty set

K10(K10( the carrier of (X,A))) is non empty set

TopStruct(# the carrier of (X,A), the topology of (X,A) #) is non empty strict TopSpace-like TopStruct

{A} is non empty trivial 1 -element Element of K10(X)

Z is non empty TopSpace-like TopStruct

the carrier of Z is non empty set

the topology of Z is non empty Element of K10(K10( the carrier of Z))

K10( the carrier of Z) is non empty set

K10(K10( the carrier of Z)) is non empty set

TopStruct(# the carrier of Z, the topology of Z #) is non empty strict TopSpace-like TopStruct

C is non empty Element of K10( the carrier of Z)

Cl C is closed Element of K10( the carrier of Z)

C \/ {A} is non empty set

C is Element of K10( the carrier of Z)

C \/ C is non empty Element of K10( the carrier of Z)

Y1 is Element of K10( the carrier of Z)

Y1 \/ C is Element of K10( the carrier of Z)

Cl (C \/ C) is closed Element of K10( the carrier of Z)

C is non empty Element of K10( the carrier of Z)

Cl C is closed Element of K10( the carrier of Z)

C \/ {A} is non empty set

C is Element of K10( the carrier of Z)

C \/ {A} is non empty set

Cl C is closed Element of K10( the carrier of Z)

Cl C is closed Element of K10( the carrier of Z)

C \/ {A} is non empty set

X is non empty set

A is Element of X

(X,A) is non empty strict TopSpace-like TopStruct

K10(X) is non empty set

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

the topology of (X,A) is non empty Element of K10(K10( the carrier of (X,A)))

K10( the carrier of (X,A)) is non empty set

K10(K10( the carrier of (X,A))) is non empty set

TopStruct(# the carrier of (X,A), the topology of (X,A) #) is non empty strict TopSpace-like TopStruct

{A} is non empty trivial 1 -element Element of K10(X)

Z is non empty TopSpace-like TopStruct

the carrier of Z is non empty set

the topology of Z is non empty Element of K10(K10( the carrier of Z))

K10( the carrier of Z) is non empty set

K10(K10( the carrier of Z)) is non empty set

TopStruct(# the carrier of Z, the topology of Z #) is non empty strict TopSpace-like TopStruct

C is Element of K10( the carrier of Z)

C /\ X is Element of K10( the carrier of Z)

Int C is open Element of K10( the carrier of Z)

C is Element of K10( the carrier of Z)

X \ C is Element of K10(X)

C \ {A} is Element of K10( the carrier of Z)

X \ {A} is Element of K10(X)

Y1 is Element of K10( the carrier of Z)

Y1 \ C is Element of K10( the carrier of Z)

C \ C is Element of K10( the carrier of Z)

Int (C \ C) is open Element of K10( the carrier of Z)

C /\ (X \ C) is Element of K10(X)

C is Element of K10( the carrier of Z)

Int C is open Element of K10( the carrier of Z)

C \ {A} is Element of K10( the carrier of Z)

C is Element of K10( the carrier of Z)

X \ {A} is Element of K10(X)

X /\ {A} is Element of K10(X)

C /\ X is Element of K10( the carrier of Z)

C /\ (X \ {A}) is Element of K10(X)

C \ {A} is Element of K10( the carrier of Z)

Int C is open Element of K10( the carrier of Z)

Int C is open Element of K10( the carrier of Z)

C \ {A} is Element of K10( the carrier of Z)

X is non empty set

Z is set

K10(X) is non empty set

A is Element of X

{ b

the Element of Z is Element of Z

{A} is non empty trivial 1 -element Element of K10(X)

C is Element of K10(X)

X \ C is Element of K10(X)

the Element of X \ C is Element of X \ C

A1 is Element of X

X is non empty set

(X) is non empty strict TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

(X) is non empty Element of K10(K10(X))

K10(X) is non empty set

K10(K10(X)) is non empty set

{{},X} is non empty set

TopStruct(# X,(X) #) is non empty strict TopStruct

A is Element of X

(X,A) is non empty strict TopSpace-like TopStruct

bool X is non empty Element of K10(K10(X))

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

{A} is non empty trivial 1 -element Element of K10(X)

X \ {A} is Element of K10(X)

the Element of X \ {A} is Element of X \ {A}

C is Element of X

{C} is non empty trivial 1 -element Element of K10(X)

Y1 is Element of K10(X)

A1 is Element of K10(X)

X is non empty set

1TopSp X is TopSpace-like discrete almost_discrete TopStruct

bool X is non empty Element of K10(K10(X))

K10(X) is non empty set

K10(K10(X)) is non empty set

[#] (bool X) is non empty non proper Element of K10((bool X))

K10((bool X)) is non empty set

TopStruct(# X,([#] (bool X)) #) is non empty strict TopStruct

A is Element of X

(X,A) is non empty strict TopSpace-like TopStruct

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

{A} is non empty trivial 1 -element Element of K10(X)

C is set

C is Element of K10(X)

C is Element of K10(X)

X is non empty set

1TopSp X is TopSpace-like discrete almost_discrete TopStruct

bool X is non empty Element of K10(K10(X))

K10(X) is non empty set

K10(K10(X)) is non empty set

[#] (bool X) is non empty non proper Element of K10((bool X))

K10((bool X)) is non empty set

TopStruct(# X,([#] (bool X)) #) is non empty strict TopStruct

A is Element of X

(X,A) is non empty strict TopSpace-like TopStruct

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

K10( the carrier of (X,A)) is non empty set

{A} is non empty trivial 1 -element Element of K10(X)

C is Element of K10( the carrier of (X,A))

(X,A) modified_with_respect_to C is non empty strict TopSpace-like TopStruct

C -extension_of_the_topology_of (X,A) is Element of K10(K10( the carrier of (X,A)))

K10(K10( the carrier of (X,A))) is non empty set

{ (b

A1 is set

Y2 is Element of K10(X)

Y2 \ {A} is Element of K10(X)

A3 is Element of K10(X)

A3 \/ C is set

Y1 is Element of K10(X)

B is Element of K10(X)

B is Element of K10(X)

Y1 /\ C is Element of K10( the carrier of (X,A))

((bool X) \ { b

(bool X) \/ { b

the topology of ((X,A) modified_with_respect_to C) is non empty Element of K10(K10( the carrier of ((X,A) modified_with_respect_to C)))

the carrier of ((X,A) modified_with_respect_to C) is non empty set

K10( the carrier of ((X,A) modified_with_respect_to C)) is non empty set

K10(K10( the carrier of ((X,A) modified_with_respect_to C))) is non empty set

the topology of (1TopSp X) is non empty Element of K10(K10( the carrier of (1TopSp X)))

the carrier of (1TopSp X) is set

K10( the carrier of (1TopSp X)) is non empty set

K10(K10( the carrier of (1TopSp X))) is non empty set

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is non empty Element of K10( the carrier of X)

Int A is open Element of K10( the carrier of X)

A is Element of K10( the carrier of X)

Z is Element of the carrier of X

{Z} is non empty trivial 1 -element Element of K10( the carrier of X)

Int A is open Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

A is Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

Z is non empty Element of K10( the carrier of X)

C is non empty Element of K10( the carrier of X)

Z is non empty Element of K10( the carrier of X)

A is non empty Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

Z is Element of K10( the carrier of X)

Z is Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is non empty Element of K10( the carrier of X)

Cl A is closed Element of K10( the carrier of X)

Int (Cl A) is open Element of K10( the carrier of X)

A is Element of K10( the carrier of X)

Z is Element of the carrier of X

{Z} is non empty trivial 1 -element Element of K10( the carrier of X)

Cl A is closed Element of K10( the carrier of X)

Fr (Cl A) is closed boundary nowhere_dense Element of K10( the carrier of X)

Int (Cl A) is open Element of K10( the carrier of X)

(Cl A) \ (Int (Cl A)) is Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

A is Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

Z is non empty Element of K10( the carrier of X)

C is non empty Element of K10( the carrier of X)

Z is non empty Element of K10( the carrier of X)

A is non empty Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

Z is Element of K10( the carrier of X)

Z is Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is non empty Element of K10( the carrier of X)

Z is Element of K10( the carrier of X)

C is non empty Element of K10( the carrier of X)

C is non empty Element of K10( the carrier of X)

A is non empty Element of K10( the carrier of X)

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is non empty Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

A is Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

Z is non empty Element of K10( the carrier of X)

C is non empty Element of K10( the carrier of X)

Z is non empty Element of K10( the carrier of X)

{{},1} is non empty set

bool {{},1} is non empty Element of K10(K10({{},1}))

K10({{},1}) is non empty set

K10(K10({{},1})) is non empty set

((bool {{},1})) is non empty strict TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

((bool {{},1})) is non empty Element of K10(K10((bool {{},1})))

K10((bool {{},1})) is non empty set

K10(K10((bool {{},1}))) is non empty set

{{},(bool {{},1})} is non empty set

TopStruct(# (bool {{},1}),((bool {{},1})) #) is non empty strict TopStruct

{{}} is non empty trivial 1 -element set

{1} is non empty trivial 1 -element Element of K10(K146())

K10(K146()) is non empty V31() set

the carrier of ((bool {{},1})) is non empty set

K10( the carrier of ((bool {{},1}))) is non empty set

C is Element of K10( the carrier of ((bool {{},1})))

((bool {{},1})) modified_with_respect_to C is non empty strict TopSpace-like TopStruct

the carrier of (((bool {{},1})) modified_with_respect_to C) is non empty set

K10( the carrier of (((bool {{},1})) modified_with_respect_to C)) is non empty set

A1 is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

A1 ` is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

the carrier of (((bool {{},1})) modified_with_respect_to C) \ A1 is set

(((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `) is non empty strict TopSpace-like TopStruct

the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)) is non empty set

K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `))) is non empty set

A2 is Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

A2 ` is Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)) \ A2 is set

Z is Element of K10({{},1})

C is Element of K10({{},1})

{Z,C} is non empty Element of K10(K10({{},1}))

A2 is set

the topology of (((bool {{},1})) modified_with_respect_to C) is non empty Element of K10(K10( the carrier of (((bool {{},1})) modified_with_respect_to C)))

K10(K10( the carrier of (((bool {{},1})) modified_with_respect_to C))) is non empty set

C -extension_of_the_topology_of ((bool {{},1})) is Element of K10(K10( the carrier of ((bool {{},1}))))

K10(K10( the carrier of ((bool {{},1})))) is non empty set

the topology of ((bool {{},1})) is non empty Element of K10(K10( the carrier of ((bool {{},1}))))

{ (b

P is Element of K10( the carrier of ((bool {{},1})))

Q is Element of K10( the carrier of ((bool {{},1})))

Q /\ C is Element of K10( the carrier of ((bool {{},1})))

P \/ (Q /\ C) is Element of K10( the carrier of ((bool {{},1})))

{{},A1,(bool {{},1})} is non empty set

A2 is set

the topology of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)) is non empty Element of K10(K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `))))

K10(K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))) is non empty set

(A1 `) -extension_of_the_topology_of (((bool {{},1})) modified_with_respect_to C) is Element of K10(K10( the carrier of (((bool {{},1})) modified_with_respect_to C)))

{ (b

P is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

Q is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

Q /\ (A1 `) is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

P \/ (Q /\ (A1 `)) is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

A1 /\ (A1 `) is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

{} (((bool {{},1})) modified_with_respect_to C) is empty proper V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

A1 /\ (A1 `) is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

{} (((bool {{},1})) modified_with_respect_to C) is empty proper V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

A1 \/ (A1 `) is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

[#] (((bool {{},1})) modified_with_respect_to C) is non empty non proper open closed dense non boundary Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C))

{{},A2,(A2 `),(bool {{},1})} is non empty set

A2 is set

A2 is Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

{} ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)) is empty proper V24() V25() V26() V28() V29() V30() V31() cardinal {} -element open closed boundary nowhere_dense Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

[#] ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)) is non empty non proper open closed dense non boundary Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

(A2 `) ` is Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)) \ (A2 `) is set

A2 is Element of the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `))

B is non empty Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

Int B is open Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

A2 is non empty Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

Int A2 is open Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

A2 is Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

A2 is Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

P is non empty Element of K10( the carrier of ((((bool {{},1})) modified_with_respect_to C) modified_with_respect_to (A1 `)))

X is non empty set

A is Element of X

{A} is non empty trivial 1 -element Element of K10(X)

K10(X) is non empty set

X \ {A} is Element of K10(X)

(X,A) is non empty strict TopSpace-like TopStruct

bool X is non empty Element of K10(K10(X))

K10(K10(X)) is non empty set

{ b

(bool X) \ { b

TopStruct(# X,((bool X) \ { b

the carrier of (X,A) is non empty set

K10( the carrier of (X,A)) is non empty set

Z is non empty Element of K10( the carrier of (X,A))

C is non empty Element of K10( the carrier of (X,A))

Z is non empty Element of K10( the carrier of (X,A))

Z is non empty Element of K10( the carrier of (X,A))

{{},1} is non empty set

A is Element of {{},1}

({{},1},A) is non empty strict TopSpace-like TopStruct

K10({{},1}) is non empty set

bool {{},1} is non empty Element of K10(K10({{},1}))

K10(K10({{},1})) is non empty set

{ b

(bool {{},1}) \ { b

TopStruct(# {{},1},((bool {{},1}) \ { b

the carrier of ({{},1},A) is non empty set

K10( the carrier of ({{},1},A)) is non empty set

{A} is non empty trivial 1 -element Element of K10({{},1})

C is non empty Element of K10( the carrier of ({{},1},A))

{{},1} \ C is Element of K10({{},1})

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is non empty Element of K10( the carrier of X)

A ` is Element of K10( the carrier of X)

the carrier of X \ A is set

X modified_with_respect_to (A `) is non empty strict TopSpace-like TopStruct

the carrier of (X modified_with_respect_to (A `)) is non empty set

K10( the carrier of (X modified_with_respect_to (A `))) is non empty set

C is non empty Element of K10( the carrier of (X modified_with_respect_to (A `)))

C is non empty Element of K10( the carrier of (X modified_with_respect_to (A `)))

C is non empty Element of K10( the carrier of (X modified_with_respect_to (A `)))

X is non empty TopSpace-like TopStruct

the carrier of X is non empty set

K10( the carrier of X) is non empty set

A is Element of K10( the carrier of X)

X modified_with_respect_to A is non empty strict TopSpace-like TopStruct

the carrier of (X modified_with_respect_to A) is non empty set

K10( the carrier of (X modified_with_respect_to A)) is non empty set

C is Element of K10( the carrier of (X modified_with_respect_to A))

C is Element of K10( the carrier of (X modified_with_respect_to A))

C is Element of K10( the carrier of (X modified_with_respect_to A))