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))
{ (b1 \/ (b2 /\ A)) where b1, b2 is Element of K10( the carrier of X) : ( b1 in the topology of X & b2 in the topology of X ) } is set
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is strict TopStruct
Z is Element of K10(X)
A1 is Element of K10(X)
the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is set
K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #)) is non empty set
K10(K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))) is non empty set
A1 is Element of K10(K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #)))
the topology of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is Element of K10(K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #)))
A1 /\ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #)))
union A1 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
union A1 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
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) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
union A1 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
A1 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
A2 is Element of K10(X)
A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
A2 is Element of K10(X)
A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
A2 is Element of K10(X)
A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
A1 /\ Y2 is Element of K10( the carrier of TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #))
{ b2 where b1 is Element of K10(X) : ( A in b2 & not b2 = X ) } is set
(bool X) \ { b2 where b1 is Element of K10(X) : ( A in b2 & not b2 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b2 where b1 is Element of K10(X) : ( A in b2 & not b2 = X ) } ) #) is strict TopStruct
the carrier of TopStruct(# X,((bool X) \ { b2 where b1 is Element of K10(X) : ( A in b2 & not b2 = X ) } ) #) is set
K10( the carrier of TopStruct(# X,((bool X) \ { b2 where b1 is Element of K10(X) : ( A in b2 & not b2 = X ) } ) #)) is non empty set
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10({{},1}) : ( A in b1 & not b1 = {{},1} ) } is set
(bool {{},1}) \ { b1 where b1 is Element of K10({{},1}) : ( A in b1 & not b1 = {{},1} ) } is Element of K10(K10({{},1}))
TopStruct(# {{},1},((bool {{},1}) \ { b1 where b1 is Element of K10({{},1}) : ( A in b1 & not b1 = {{},1} ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
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))
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
{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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
{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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ (b1 \/ (b2 /\ C)) where b1, b2 is Element of K10( the carrier of (X,A)) : ( b1 in (bool X) \ { b1 where b3 is Element of K10(X) : ( A in b1 & not b1 = X ) } & b2 in (bool X) \ { b1 where b3 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) } is set
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) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) \/ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \/ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is non empty set
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}))))
{ (b1 \/ (b2 /\ C)) where b1, b2 is Element of K10( the carrier of ((bool {{},1}))) : ( b1 in the topology of ((bool {{},1})) & b2 in the topology of ((bool {{},1})) ) } is set
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)))
{ (b1 \/ (b2 /\ (A1 `))) where b1, b2 is Element of K10( the carrier of (((bool {{},1})) modified_with_respect_to C)) : ( b1 in the topology of (((bool {{},1})) modified_with_respect_to C) & b2 in the topology of (((bool {{},1})) modified_with_respect_to C) ) } is set
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
{ b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is set
(bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } is Element of K10(K10(X))
TopStruct(# X,((bool X) \ { b1 where b1 is Element of K10(X) : ( A in b1 & not b1 = X ) } ) #) is non empty strict TopStruct
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
{ b1 where b1 is Element of K10({{},1}) : ( A in b1 & not b1 = {{},1} ) } is set
(bool {{},1}) \ { b1 where b1 is Element of K10({{},1}) : ( A in b1 & not b1 = {{},1} ) } is Element of K10(K10({{},1}))
TopStruct(# {{},1},((bool {{},1}) \ { b1 where b1 is Element of K10({{},1}) : ( A in b1 & not b1 = {{},1} ) } ) #) is non empty strict TopStruct
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))