K125() is set
K10(K125()) is non empty set
K185() is non empty strict TopSpace-like TopStruct
the carrier of K185() is non empty set
{} is empty set
the empty set is empty set
1 is non empty set
union {} is set
X is TopSpace-like TopStruct
the carrier of X is 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)
A ` is Element of K10( the carrier of X)
the carrier of X \ A is set
Int (A `) is open Element of K10( the carrier of X)
(Int (A `)) ` is closed Element of K10( the carrier of X)
the carrier of X \ (Int (A `)) is set
(A `) ` is Element of K10( the carrier of X)
the carrier of X \ (A `) is set
Cl ((A `) `) is closed Element of K10( the carrier of X)
(Cl ((A `) `)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl ((A `) `)) is set
((Cl ((A `) `)) `) ` is closed Element of K10( the carrier of X)
the carrier of X \ ((Cl ((A `) `)) `) is set
X is TopSpace-like TopStruct
the carrier of X is 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
Cl (A `) is closed Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
(Int A) ` is closed Element of K10( the carrier of X)
the carrier of X \ (Int A) is set
(A `) ` is Element of K10( the carrier of X)
the carrier of X \ (A `) is set
Int ((A `) `) is open Element of K10( the carrier of X)
(Int ((A `) `)) ` is closed Element of K10( the carrier of X)
the carrier of X \ (Int ((A `) `)) is set
X is TopSpace-like TopStruct
the carrier of X is 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
Int (A `) is open Element of K10( the carrier of X)
Cl A is closed Element of K10( the carrier of X)
(Cl A) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl A) is set
(A `) ` is Element of K10( the carrier of X)
the carrier of X \ (A `) is set
Cl ((A `) `) is closed Element of K10( the carrier of X)
(Cl ((A `) `)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl ((A `) `)) is set
X is TopSpace-like TopStruct
the carrier of X is 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 \/ A is Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
A \/ (Int A) is Element of K10( the carrier of X)
(A \/ A) ` is Element of K10( the carrier of X)
the carrier of X \ (A \/ A) is set
{} X is empty open closed boundary nowhere_dense 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)
the carrier of X \ A is set
(A `) /\ (A `) is Element of K10( the carrier of X)
Cl (A `) is closed Element of K10( the carrier of X)
(Cl (A `)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl (A `)) is set
((Cl (A `)) `) ` is closed Element of K10( the carrier of X)
the carrier of X \ ((Cl (A `)) `) is set
(A `) /\ (((Cl (A `)) `) `) is Element of K10( the carrier of X)
(Int A) ` is closed Element of K10( the carrier of X)
the carrier of X \ (Int A) is set
(A `) /\ ((Int A) `) is Element of K10( the carrier of X)
(A \/ (Int A)) ` is Element of K10( the carrier of X)
the carrier of X \ (A \/ (Int A)) is set
((A \/ (Int A)) `) ` is Element of K10( the carrier of X)
the carrier of X \ ((A \/ (Int A)) `) is set
[#] X is non proper open closed dense Element of K10( the carrier of X)
X is TopSpace-like TopStruct
the carrier of X is 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 TopSpace-like TopStruct
the carrier of X is 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 (Cl A) is open Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
Cl (Int A) is closed Element of K10( the carrier of X)
X is TopSpace-like TopStruct
the carrier of X is 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)
Cl (Int A) is closed 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)
X is TopSpace-like TopStruct
the carrier of X is 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)
Cl (Int A) is closed 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)
X is TopSpace-like TopStruct
the carrier of X is 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 (Cl A) is open Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
Cl (Int A) is closed Element of K10( the carrier of X)
Int (Int (Cl A)) is open Element of K10( the carrier of X)
Cl (Cl (Int A)) is closed Element of K10( the carrier of X)
X is TopStruct
the carrier of X is 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 topology of X is Element of K10(K10( the carrier of X))
X is TopStruct
the topology of X is Element of K10(K10( the carrier of X))
the carrier of X is set
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
{{}} is non empty set
K10({{}}) is non empty set
K10(K10({{}})) is non empty set
bool {{}} is non empty Element of K10(K10({{}}))
A is Element of K10(K10({{}}))
TopStruct(# {{}},A #) is non empty strict TopStruct
A is non empty strict TopStruct
{{},{{}}} is non empty set
X is () TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
the topology of X is Element of K10(K10( the carrier of X))
K10(K10( the carrier of X)) is non empty set
A is Element of K10( the carrier of X)
the carrier of X \ A is Element of K10( the carrier of X)
bool the carrier of X is non empty Element of K10(K10( the carrier of X))
X is () TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
the topology of X is Element of K10(K10( the carrier of X))
K10(K10( the carrier of X)) is non empty set
A is Element of K10( the carrier of X)
the carrier of X \ A is Element of K10( the carrier of X)
{{}, the carrier of X} is non empty set
X is TopStruct
the topology of X is Element of K10(K10( the carrier of X))
the carrier of X is set
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))
A is Element of K10(K10( the carrier of X))
union 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)
A /\ A is Element of K10( the carrier of X)
X is TopStruct
the topology of X is Element of K10(K10( the carrier of X))
the carrier of X is set
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
A is Element of K10( the carrier of X)
A is Element of K10( the carrier of X)
A /\ A is Element of K10( the carrier of X)
A is Element of K10(K10( the carrier of X))
union A is Element of K10( the carrier of X)
{{}} is non empty set
{ the carrier of X} is non empty set
{} \/ the carrier of X is set
X is TopSpace-like TopStruct
the carrier of X is 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
A is Element of K10(K10( the carrier of X))
the topology of X is non empty Element of K10(K10( the carrier of X))
A is Element of K10(K10( the carrier of X))
X is TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
the topology of X is Element of K10(K10( the carrier of X))
K10(K10( the carrier of X)) is non empty set
A is Element of K10( the carrier of X)
the carrier of X \ A is Element of K10( the carrier of X)
X is TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
the topology of X is Element of K10(K10( the carrier of X))
K10(K10( the carrier of X)) is non empty set
A is Element of K10( the carrier of X)
the carrier of X \ A is Element of K10( the carrier of X)
the strict TopSpace-like () () TopStruct is strict TopSpace-like () () TopStruct
the non empty strict TopSpace-like () () () TopStruct is non empty strict TopSpace-like () () () TopStruct
A is TopSpace-like TopStruct
X is TopSpace-like TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
A is Element of K10( the carrier of X)
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
bool the carrier of X is non empty Element of K10(K10( the carrier of X))
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
bool the carrier of X is non empty Element of K10(K10( the carrier of X))
A is set
A is Element of K10( the carrier of X)
X is TopSpace-like TopStruct
the carrier of X is 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
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 is TopSpace-like TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
A is Element of K10( the carrier of X)
{ b1 where b1 is Element of K10( the carrier of X) : ex b2 being Element of the carrier of X st
( b2 in A & b1 = {b2} ) } is set
bool A is non empty Element of K10(K10(A))
K10(A) is non empty set
K10(K10(A)) is non empty set
C is set
B is Element of K10( the carrier of X)
c is Element of the carrier of X
{c} is non empty set
bool the carrier of X is non empty Element of K10(K10( the carrier of X))
K10(K10( the carrier of X)) is non empty set
union (bool A) is Element of K10(A)
B is set
a is set
c is Element of K10( the carrier of X)
b is Element of the carrier of X
{b} is non empty set
P0 is non empty set
C is Element of K10(K10( the carrier of X))
union C is Element of K10( the carrier of X)
P0 is non empty set
B 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 set
X is non empty TopSpace-like () () TopStruct
A is TopSpace-like SubSpace of X
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)
the carrier of A is set
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)
the carrier of A is set
the topology of X is non empty Element of K10(K10( the carrier of X))
the carrier of X is non empty set
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))
A is set
the carrier of A is set
bool the carrier of A is non empty Element of K10(K10( the carrier of A))
K10( the carrier of A) is non empty set
K10(K10( the carrier of A)) is non empty set
C is Element of K10( the carrier of A)
B is Element of K10( the carrier of X)
c is Element of K10( the carrier of X)
[#] A is non proper open closed dense Element of K10( the carrier of A)
c /\ ([#] A) is Element of K10( the carrier of A)
the topology of A is non empty Element of K10(K10( the carrier of A))
c is Element of K10( the carrier of X)
c /\ ([#] A) is Element of K10( the carrier of A)
X is non empty TopSpace-like () () TopStruct
the strict TopSpace-like closed open () () SubSpace of X is strict TopSpace-like closed open () () SubSpace of X
X is TopSpace-like TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
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 is Element of K10( the carrier of X)
{{}, the carrier of X} is non empty set
A is set
A is Element of K10( the carrier of X)
{{}, the carrier of X} is non empty set
X is TopSpace-like TopStruct
the carrier of X is 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
(A `) ` is Element of K10( the carrier of X)
the carrier of X \ (A `) is set
[#] X is non proper open closed dense Element of K10( the carrier of X)
{} X is empty open closed boundary nowhere_dense 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
(A `) ` is Element of K10( the carrier of X)
the carrier of X \ (A `) is set
[#] X is non proper open closed dense Element of K10( the carrier of X)
{} X is empty open closed boundary nowhere_dense Element of K10( the carrier of X)
X is TopSpace-like TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
A is Element of K10( the carrier of X)
the Element of A is Element of A
C is Element of the carrier of X
{C} is non empty set
B is Element of K10( the carrier of X)
Cl B is closed Element of K10( the carrier of X)
X is non empty TopSpace-like () () TopStruct
A is TopSpace-like SubSpace of X
the topology of X is non empty Element of K10(K10( the carrier of X))
the carrier of X is non empty set
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
A is set
the topology of A is non empty Element of K10(K10( the carrier of A))
the carrier of A is set
K10( the carrier of A) is non empty set
K10(K10( the carrier of A)) is non empty set
C is Element of K10( the carrier of A)
[#] A is non proper open closed dense Element of K10( the carrier of A)
B is Element of K10( the carrier of X)
B /\ ([#] A) is Element of K10( the carrier of A)
{{}, the carrier of A} is non empty set
A is set
X is non empty TopSpace-like () () TopStruct
the TopSpace-like () () SubSpace of X is TopSpace-like () () SubSpace of X
X is TopSpace-like TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
A is Element of K10( the carrier of X)
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
the carrier of X \ A is Element of K10( the carrier of X)
[#] X is non proper open closed dense Element of K10( the carrier of X)
([#] X) \ 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 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 is Element of K10( the carrier of X)
[#] X is non proper open closed dense Element of K10( the carrier of X)
([#] X) \ A is Element of K10( the carrier of X)
the carrier of X \ A is Element of K10( the carrier of X)
X is TopSpace-like TopStruct
the carrier of X is 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
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 is TopSpace-like TopStruct
the carrier of X is 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)
A is Element of K10( the carrier of X)
Cl A is closed Element of K10( the carrier of X)
X is TopSpace-like TopStruct
the carrier of X is 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)
A is Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
the strict TopSpace-like () () TopStruct is strict TopSpace-like () () TopStruct
X is TopSpace-like TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
A is Element of K10( the carrier of X)
{ b1 where b1 is Element of K10( the carrier of X) : ex b2 being Element of K10( the carrier of X) ex b3 being Element of the carrier of X st
( b3 in A & b2 = {b3} & b1 = Cl b2 ) } is set
bool A is non empty Element of K10(K10(A))
K10(A) is non empty set
K10(K10(A)) is non empty set
union (bool A) is Element of K10(A)
C is Element of K10( the carrier of X)
Cl C is closed Element of K10( the carrier of X)
B is Element of the carrier of X
{B} is non empty set
Cl A is closed Element of K10( the carrier of X)
C is set
B is Element of K10( the carrier of X)
a is Element of the carrier of X
c is Element of K10( the carrier of X)
{a} is non empty set
Cl c is closed Element of K10( the carrier of X)
bool the carrier of X is non empty Element of K10(K10( the carrier of X))
K10(K10( the carrier of X)) is non empty set
B is set
a is set
c is Element of K10( the carrier of X)
b is Element of the carrier of X
{b} is non empty set
P0 is Element of K10( the carrier of X)
Cl P0 is closed Element of K10( the carrier of X)
B is closed Element of K10( the carrier of X)
C is Element of K10(K10( the carrier of X))
union C is Element of K10( the carrier of X)
P0 is closed Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
c is Element of K10( the carrier of X)
b is Element of the carrier of X
a is Element of K10( the carrier of X)
{b} is non empty set
Cl a is closed Element of K10( the carrier of X)
X is TopSpace-like TopStruct
the carrier of X is set
K10( the carrier of X) is non empty set
A is Element of K10( the carrier of X)
A is Element of the carrier of X
{A} is non empty set
A is Element of K10( the carrier of X)
A is Element of the carrier of X
{A} is non empty set
X is TopSpace-like TopStruct
X is TopSpace-like TopStruct
X is non empty TopSpace-like () TopStruct
A is non empty TopSpace-like SubSpace of X
the carrier of A is non empty set
K10( the carrier of A) is non empty set
A is Element of K10( the carrier of A)
the carrier of X is non empty set
K10( the carrier of X) is non empty set
[#] A is non empty non proper open closed dense non boundary Element of K10( the carrier of A)
C is Element of K10( the carrier of X)
C /\ ([#] A) is Element of K10( the carrier of A)
X is non empty TopSpace-like () TopStruct
A is TopSpace-like SubSpace of X
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)
the carrier of A is set
A is TopSpace-like SubSpace of X
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)
the carrier of A is set
X is non empty TopSpace-like () TopStruct
the non empty strict TopSpace-like () SubSpace of X is non empty strict TopSpace-like () SubSpace of X
the non empty strict TopSpace-like () () TopStruct is non empty strict TopSpace-like () () TopStruct
the carrier of the non empty strict TopSpace-like () () TopStruct is non empty set
K10( the carrier of the non empty strict TopSpace-like () () TopStruct ) is non empty set
A is Element of K10( the carrier of the non empty strict TopSpace-like () () TopStruct )
Cl A is closed Element of K10( the carrier of the non empty strict 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 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)
the carrier of X \ A is set
Cl (A `) is closed Element of K10( the carrier of X)
(Cl (A `)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl (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
Int (A `) is open Element of K10( the carrier of X)
(Int (A `)) ` is closed Element of K10( the carrier of X)
the carrier of X \ (Int (A `)) is set
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)
A is Element of K10( the carrier of X)
Cl A is closed Element of K10( the carrier of X)
Cl A is closed Element of K10( the carrier of X)
A is Element of K10( the carrier of X)
Cl A is closed Element of K10( the carrier of X)
(Cl A) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl A) is set
Cl ((Cl A) `) is closed Element of K10( the carrier of X)
(Cl ((Cl A) `)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl ((Cl A) `)) is set
Int (Cl 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 \/ A is Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
(Int A) \/ (Int A) is open Element of K10( the carrier of X)
(A \/ A) ` is Element of K10( the carrier of X)
the carrier of X \ (A \/ A) is set
{} X is empty proper open closed boundary nowhere_dense 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)
the carrier of X \ A is set
(A `) /\ (A `) is Element of K10( the carrier of X)
Cl (A `) is closed Element of K10( the carrier of X)
Cl (A `) is closed Element of K10( the carrier of X)
(Cl (A `)) /\ (Cl (A `)) is closed Element of K10( the carrier of X)
((Cl (A `)) /\ (Cl (A `))) ` is open Element of K10( the carrier of X)
the carrier of X \ ((Cl (A `)) /\ (Cl (A `))) is set
[#] X is non empty non proper open closed dense non boundary Element of K10( the carrier of X)
(Cl (A `)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl (A `)) is set
(Cl (A `)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl (A `)) is set
((Cl (A `)) `) \/ ((Cl (A `)) `) is open Element of K10( the carrier of X)
((Cl (A `)) `) \/ (Int A) is open 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)
A /\ A is Element of K10( the carrier of X)
{} X is empty proper open closed boundary nowhere_dense Element of K10( the carrier of X)
(A /\ A) ` is Element of K10( the carrier of X)
the carrier of X \ (A /\ A) is set
[#] X is non empty non proper open closed dense non boundary 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)
the carrier of X \ A is set
(A `) \/ (A `) is Element of K10( the carrier of X)
Int (A `) is open Element of K10( the carrier of X)
Int (A `) is open Element of K10( the carrier of X)
(Int (A `)) \/ (Int (A `)) is open Element of K10( the carrier of X)
((Int (A `)) \/ (Int (A `))) ` is closed Element of K10( the carrier of X)
the carrier of X \ ((Int (A `)) \/ (Int (A `))) is set
(Int (A `)) ` is closed Element of K10( the carrier of X)
the carrier of X \ (Int (A `)) is set
(Int (A `)) ` is closed Element of K10( the carrier of X)
the carrier of X \ (Int (A `)) is set
((Int (A `)) `) /\ ((Int (A `)) `) is closed Element of K10( the carrier of X)
Cl A is closed Element of K10( the carrier of X)
(Cl A) /\ ((Int (A `)) `) is closed 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)
Cl A is closed Element of K10( the carrier of X)
Int (Cl A) is open Element of K10( the carrier of X)
(Cl A) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl A) is set
Cl ((Cl A) `) is closed Element of K10( the carrier of X)
(Cl ((Cl A) `)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl ((Cl A) `)) is set
A is 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)
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)
Cl (Int A) is closed Element of K10( the carrier of X)
A ` is Element of K10( the carrier of X)
the carrier of X \ A is set
Cl (A `) is closed Element of K10( the carrier of X)
Int (Cl (A `)) is open Element of K10( the carrier of X)
(Cl (A `)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl (A `)) is set
((Cl (A `)) `) ` is closed Element of K10( the carrier of X)
the carrier of X \ ((Cl (A `)) `) is set
Int (((Cl (A `)) `) `) is open Element of K10( the carrier of X)
(Int (((Cl (A `)) `) `)) ` is closed Element of K10( the carrier of X)
the carrier of X \ (Int (((Cl (A `)) `) `)) is set
Cl ((Cl (A `)) `) is closed Element of K10( the carrier of X)
A is Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
Cl (Int 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)
Cl (Int A) is closed 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)
Int A is open Element of K10( the carrier of X)
Cl (Int A) is closed 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)
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)
Cl A is closed Element of K10( the carrier of X)
Int (Cl A) is open Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
Cl (Int A) is closed Element of K10( the carrier of X)
A is 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)
Int A is open Element of K10( the carrier of X)
Cl (Int 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)
Cl A is closed Element of K10( the carrier of X)
A is Element of K10( the carrier of X)
Int A is open 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)
A is 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)
Int A is open Element of K10( the carrier of X)
Cl (Int A) is closed Element of K10( the carrier of X)
Cl (Cl (Int A)) is closed Element of K10( the carrier of X)
Int (Cl (Cl (Int A))) is open Element of K10( the carrier of X)
the non empty strict TopSpace-like () () TopStruct is non empty strict TopSpace-like () () TopStruct
A is non empty TopSpace-like closed open () () SubSpace of the non empty strict TopSpace-like () () TopStruct
the carrier of A is non empty set
K10( the carrier of A) is non empty set
A is Element of K10( the carrier of A)
Cl A is closed Element of K10( the carrier of A)
X is non empty TopSpace-like TopStruct
X is non empty TopSpace-like TopStruct
A is non empty TopSpace-like () TopStruct
A is non empty TopSpace-like () SubSpace of A
the carrier of A is non empty set
K10( the carrier of A) is non empty set
C is Element of K10( the carrier of A)
Cl C is closed Element of K10( the carrier of 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 non empty TopSpace-like SubSpace of X
the carrier of A is non empty set
A is Element of K10( the carrier of X)
K10( the carrier of A) is non empty set
C is Element of K10( the carrier of A)
B is Element of K10( the carrier of A)
Cl C is closed Element of K10( the carrier of A)
Cl B is closed Element of K10( the carrier of A)
[#] A is non empty non proper open closed dense non boundary Element of K10( the carrier of A)
c is Element of K10( the carrier of X)
c /\ ([#] A) is Element of K10( the carrier of A)
a is Element of K10( the carrier of X)
a /\ ([#] A) is Element of K10( the carrier of A)
C /\ B is Element of K10( the carrier of A)
c /\ a is Element of K10( the carrier of X)
(c /\ a) /\ A is Element of K10( the carrier of X)
A /\ A is Element of K10( the carrier of X)
a /\ (A /\ A) is Element of K10( the carrier of X)
c /\ (a /\ (A /\ A)) is Element of K10( the carrier of X)
a /\ A is Element of K10( the carrier of X)
A /\ (a /\ A) is Element of K10( the carrier of X)
c /\ (A /\ (a /\ A)) is Element of K10( the carrier of X)
Cl c is closed Element of K10( the carrier of X)
Cl a is closed Element of K10( the carrier of X)
(Cl c) /\ (Cl a) is closed Element of K10( the carrier of X)
((Cl c) /\ (Cl a)) /\ ([#] A) is Element of K10( the carrier of A)
([#] A) /\ ([#] A) is open closed Element of K10( the carrier of A)
(Cl a) /\ (([#] A) /\ ([#] A)) is Element of K10( the carrier of A)
(Cl c) /\ ((Cl a) /\ (([#] A) /\ ([#] A))) is Element of K10( the carrier of A)
(Cl a) /\ ([#] A) is Element of K10( the carrier of A)
([#] A) /\ ((Cl a) /\ ([#] A)) is Element of K10( the carrier of A)
(Cl c) /\ (([#] A) /\ ((Cl a) /\ ([#] A))) is Element of K10( the carrier of A)
(Cl c) /\ ([#] A) is Element of K10( the carrier of A)
((Cl c) /\ ([#] A)) /\ ((Cl a) /\ ([#] A)) is Element of K10( the carrier of A)
b is Element of K10( the carrier of X)
Cl b is closed Element of K10( the carrier of X)
(Cl b) /\ ([#] A) is Element of K10( the carrier of A)
b is Element of K10( the carrier of X)
Cl b is closed Element of K10( the carrier of X)
(Cl b) /\ ([#] A) is Element of K10( the carrier of A)
(Cl C) /\ (Cl B) is closed Element of K10( the carrier of A)
X is non empty TopSpace-like () TopStruct
A is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is non empty set
the carrier of A is non empty set
K10( the carrier of A) is non empty set
C is Element of K10( the carrier of A)
A is Element of K10( the carrier of X)
B is Element of K10( the carrier of X)
Cl B is closed Element of K10( the carrier of X)
Cl C is closed Element of K10( the carrier of A)
[#] A is non empty non proper open closed dense non boundary Element of K10( the carrier of A)
(Cl B) /\ ([#] A) is Element of K10( the carrier of A)
X is non empty TopSpace-like () TopStruct
the non empty strict TopSpace-like open () SubSpace of X is non empty strict TopSpace-like open () SubSpace of X
X is non empty TopSpace-like () () TopStruct
A is non empty TopSpace-like SubSpace of X
A is non empty TopSpace-like SubSpace of A
X is non empty TopSpace-like () () TopStruct
the non empty strict TopSpace-like () () SubSpace of X is non empty strict TopSpace-like () () SubSpace of X
X is non empty TopSpace-like TopStruct
A is non empty TopSpace-like SubSpace of X
the carrier of X is non empty set
K10( the carrier of X) is non empty set
the carrier of A is non empty set
A is Element of K10( the carrier of X)
Cl A is closed Element of K10( the carrier of X)
B is non empty strict TopSpace-like closed SubSpace of X
the carrier of B is non empty set
K10( the carrier of B) is non empty set
c is non empty TopSpace-like SubSpace of B
the carrier of c is non empty set
a is Element of K10( the carrier of B)
Cl a is closed Element of K10( the carrier of B)
[#] B is non empty non proper open closed dense non boundary Element of K10( the carrier of B)
(Cl A) /\ ([#] B) is Element of K10( the carrier of B)
X is non empty TopSpace-like () TopStruct
Domains_of X is Element of K10(K10( the carrier of X))
the carrier of X is non empty set
K10( the carrier of X) is non empty set
K10(K10( the carrier of X)) is non empty set
Closed_Domains_of X is Element of K10(K10( the carrier of X))
A is set
A is Element of K10( the carrier of X)
{ b1 where b1 is Element of K10( the carrier of X) : b1 is condensed } is set
C is Element of K10( the carrier of X)
{ b1 where b1 is Element of K10( the carrier of X) : b1 is closed_condensed } is set
X is non empty TopSpace-like () TopStruct
Domains_Union X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
Domains_of X is Element of K10(K10( the carrier of X))
the carrier of X is non empty set
K10( the carrier of X) is non empty set
K10(K10( the carrier of X)) is non empty set
K11((Domains_of X),(Domains_of X)) is set
K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)) is set
K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X))) is non empty set
Closed_Domains_Union X is V7() V10(K11((Closed_Domains_of X),(Closed_Domains_of X))) V11( Closed_Domains_of X) V12() V21(K11((Closed_Domains_of X),(Closed_Domains_of X)), Closed_Domains_of X) Element of K10(K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X)))
Closed_Domains_of X is Element of K10(K10( the carrier of X))
K11((Closed_Domains_of X),(Closed_Domains_of X)) is set
K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X)) is set
K10(K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X))) is non empty set
Domains_Meet X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
Closed_Domains_Meet X is V7() V10(K11((Closed_Domains_of X),(Closed_Domains_of X))) V11( Closed_Domains_of X) V12() V21(K11((Closed_Domains_of X),(Closed_Domains_of X)), Closed_Domains_of X) Element of K10(K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X)))
(Domains_Union X) || (Closed_Domains_of X) is set
K37((Domains_Union X),K11((Closed_Domains_of X),(Closed_Domains_of X))) is V7() set
(Domains_Meet X) || (Closed_Domains_of X) is set
K37((Domains_Meet X),K11((Closed_Domains_of X),(Closed_Domains_of X))) is V7() set
X is non empty TopSpace-like () TopStruct
Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented LattStr
Closed_Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean LattStr
Domains_Union X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
Domains_of X is Element of K10(K10( the carrier of X))
the carrier of X is non empty set
K10( the carrier of X) is non empty set
K10(K10( the carrier of X)) is non empty set
K11((Domains_of X),(Domains_of X)) is set
K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)) is set
K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X))) is non empty set
Closed_Domains_Union X is V7() V10(K11((Closed_Domains_of X),(Closed_Domains_of X))) V11( Closed_Domains_of X) V12() V21(K11((Closed_Domains_of X),(Closed_Domains_of X)), Closed_Domains_of X) Element of K10(K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X)))
Closed_Domains_of X is Element of K10(K10( the carrier of X))
K11((Closed_Domains_of X),(Closed_Domains_of X)) is set
K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X)) is set
K10(K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X))) is non empty set
Domains_Meet X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
Closed_Domains_Meet X is V7() V10(K11((Closed_Domains_of X),(Closed_Domains_of X))) V11( Closed_Domains_of X) V12() V21(K11((Closed_Domains_of X),(Closed_Domains_of X)), Closed_Domains_of X) Element of K10(K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X)))
LattStr(# (Closed_Domains_of X),(Closed_Domains_Union X),(Closed_Domains_Meet X) #) is strict LattStr
X is non empty TopSpace-like () TopStruct
Domains_of X is Element of K10(K10( the carrier of X))
the carrier of X is non empty set
K10( the carrier of X) is non empty set
K10(K10( the carrier of X)) is non empty set
Open_Domains_of X is Element of K10(K10( the carrier of X))
A is set
A is Element of K10( the carrier of X)
{ b1 where b1 is Element of K10( the carrier of X) : b1 is condensed } is set
C is Element of K10( the carrier of X)
{ b1 where b1 is Element of K10( the carrier of X) : b1 is open_condensed } is set
X is non empty TopSpace-like () TopStruct
Domains_Union X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
Domains_of X is Element of K10(K10( the carrier of X))
the carrier of X is non empty set
K10( the carrier of X) is non empty set
K10(K10( the carrier of X)) is non empty set
K11((Domains_of X),(Domains_of X)) is set
K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)) is set
K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X))) is non empty set
Open_Domains_Union X is V7() V10(K11((Open_Domains_of X),(Open_Domains_of X))) V11( Open_Domains_of X) V12() V21(K11((Open_Domains_of X),(Open_Domains_of X)), Open_Domains_of X) Element of K10(K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X)))
Open_Domains_of X is Element of K10(K10( the carrier of X))
K11((Open_Domains_of X),(Open_Domains_of X)) is set
K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X)) is set
K10(K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X))) is non empty set
Domains_Meet X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
Open_Domains_Meet X is V7() V10(K11((Open_Domains_of X),(Open_Domains_of X))) V11( Open_Domains_of X) V12() V21(K11((Open_Domains_of X),(Open_Domains_of X)), Open_Domains_of X) Element of K10(K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X)))
(Domains_Union X) || (Open_Domains_of X) is set
K37((Domains_Union X),K11((Open_Domains_of X),(Open_Domains_of X))) is V7() set
(Domains_Meet X) || (Open_Domains_of X) is set
K37((Domains_Meet X),K11((Open_Domains_of X),(Open_Domains_of X))) is V7() set
X is non empty TopSpace-like () TopStruct
Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented LattStr
Open_Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean LattStr
Domains_Union X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
Domains_of X is Element of K10(K10( the carrier of X))
the carrier of X is non empty set
K10( the carrier of X) is non empty set
K10(K10( the carrier of X)) is non empty set
K11((Domains_of X),(Domains_of X)) is set
K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)) is set
K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X))) is non empty set
Open_Domains_Union X is V7() V10(K11((Open_Domains_of X),(Open_Domains_of X))) V11( Open_Domains_of X) V12() V21(K11((Open_Domains_of X),(Open_Domains_of X)), Open_Domains_of X) Element of K10(K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X)))
Open_Domains_of X is Element of K10(K10( the carrier of X))
K11((Open_Domains_of X),(Open_Domains_of X)) is set
K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X)) is set
K10(K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X))) is non empty set
Domains_Meet X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
Open_Domains_Meet X is V7() V10(K11((Open_Domains_of X),(Open_Domains_of X))) V11( Open_Domains_of X) V12() V21(K11((Open_Domains_of X),(Open_Domains_of X)), Open_Domains_of X) Element of K10(K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X)))
LattStr(# (Open_Domains_of X),(Open_Domains_Union X),(Open_Domains_Meet X) #) is strict LattStr
X is non empty TopSpace-like () TopStruct
Domains_of X is Element of K10(K10( the carrier of X))
the carrier of X is non empty set
K10( the carrier of X) is non empty set
K10(K10( the carrier of X)) is non empty set
Domains_Union X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
K11((Domains_of X),(Domains_of X)) is set
K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)) is set
K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X))) is non empty set
Domains_Meet X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
A is Element of Domains_of X
A is Element of Domains_of X
(Domains_Union X) . (A,A) is Element of Domains_of X
A \/ A is set
(Domains_Meet X) . (A,A) is Element of Domains_of X
A /\ A is set
Closed_Domains_of X is Element of K10(K10( the carrier of X))
Closed_Domains_Union X is V7() V10(K11((Closed_Domains_of X),(Closed_Domains_of X))) V11( Closed_Domains_of X) V12() V21(K11((Closed_Domains_of X),(Closed_Domains_of X)), Closed_Domains_of X) Element of K10(K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X)))
K11((Closed_Domains_of X),(Closed_Domains_of X)) is set
K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X)) is set
K10(K11(K11((Closed_Domains_of X),(Closed_Domains_of X)),(Closed_Domains_of X))) is non empty set
C is Element of Closed_Domains_of X
B is Element of Closed_Domains_of X
(Closed_Domains_Union X) . (C,B) is Element of Closed_Domains_of X
Open_Domains_of X is Element of K10(K10( the carrier of X))
Open_Domains_Meet X is V7() V10(K11((Open_Domains_of X),(Open_Domains_of X))) V11( Open_Domains_of X) V12() V21(K11((Open_Domains_of X),(Open_Domains_of X)), Open_Domains_of X) Element of K10(K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X)))
K11((Open_Domains_of X),(Open_Domains_of X)) is set
K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X)) is set
K10(K11(K11((Open_Domains_of X),(Open_Domains_of X)),(Open_Domains_of X))) is non empty set
c is Element of Open_Domains_of X
a is Element of Open_Domains_of X
(Open_Domains_Meet X) . (c,a) is Element of Open_Domains_of X
X is non empty TopSpace-like () TopStruct
Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented LattStr
the carrier of (Domains_Lattice X) is non empty set
Domains_of X is Element of K10(K10( the carrier of X))
the carrier of X is non empty 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 (Domains_Lattice X)
A is Element of the carrier of (Domains_Lattice X)
A "\/" A is Element of the carrier of (Domains_Lattice X)
A "/\" A is Element of the carrier of (Domains_Lattice X)
C is Element of Domains_of X
B is Element of Domains_of X
C \/ B is set
C /\ B is set
Domains_Union X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
K11((Domains_of X),(Domains_of X)) is set
K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)) is set
K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X))) is non empty set
Domains_Meet X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
LattStr(# (Domains_of X),(Domains_Union X),(Domains_Meet X) #) is strict LattStr
(Domains_Union X) . (C,B) is Element of Domains_of X
(Domains_Meet X) . (C,B) is Element of Domains_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
K10(K10( the carrier of X)) is non empty set
Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented LattStr
the carrier of (Domains_Lattice X) is non empty set
K10( the carrier of (Domains_Lattice X)) is non empty set
A is Element of K10(K10( the carrier of X))
union A is Element of K10( the carrier of X)
Cl (union A) is closed Element of K10( the carrier of X)
Domains_of X is Element of K10(K10( the carrier of X))
Closed_Domains_of X is Element of K10(K10( the carrier of X))
A is Element of K10( the carrier of (Domains_Lattice X))
"\/" (A,(Domains_Lattice X)) is Element of the carrier of (Domains_Lattice X)
Closed_Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean LattStr
the carrier of (Closed_Domains_Lattice X) is non empty set
K10( the carrier of (Closed_Domains_Lattice X)) is non empty set
C is Element of K10( the carrier of (Closed_Domains_Lattice X))
"\/" (C,(Closed_Domains_Lattice X)) is Element of the carrier of (Closed_Domains_Lattice 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
K10(K10( the carrier of X)) is non empty set
Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented LattStr
the carrier of (Domains_Lattice X) is non empty set
K10( the carrier of (Domains_Lattice X)) is non empty set
[#] X is non empty non proper open closed dense non boundary Element of K10( the carrier of X)
A is Element of K10(K10( the carrier of X))
meet A is Element of K10( the carrier of X)
Int (meet A) is open Element of K10( the carrier of X)
Domains_of X is Element of K10(K10( the carrier of X))
Open_Domains_of X is Element of K10(K10( the carrier of X))
A is Element of K10( the carrier of (Domains_Lattice X))
"/\" (A,(Domains_Lattice X)) is Element of the carrier of (Domains_Lattice X)
Open_Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean LattStr
X is non empty TopSpace-like TopStruct
Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented LattStr
Open_Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean LattStr
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 (Cl A) is open Element of K10( the carrier of X)
Int A is open Element of K10( the carrier of X)
Cl (Int A) is closed Element of K10( the carrier of X)
(Cl (Int A)) ` is open Element of K10( the carrier of X)
the carrier of X \ (Cl (Int A)) is set
Cl (Int (Cl A)) is closed Element of K10( the carrier of X)
Int (Cl (Int (Cl A))) is open Element of K10( the carrier of X)
((Cl (Int A)) `) /\ (Cl (Int A)) is Element of K10( the carrier of X)
{} X is empty proper open closed boundary nowhere_dense Element of K10( the carrier of X)
Int (Cl (Int A)) is open Element of K10( the carrier of X)
Cl (Int (Cl (Int A))) is closed Element of K10( the carrier of X)
{ b1 where b1 is Element of K10( the carrier of X) : b1 is condensed } is set
Domains_of X is Element of K10(K10( the carrier of X))
K10(K10( the carrier of X)) is non empty set
Domains_Union X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
K11((Domains_of X),(Domains_of X)) is set
K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)) is set
K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X))) is non empty set
Domains_Meet X is V7() V10(K11((Domains_of X),(Domains_of X))) V11( Domains_of X) V12() V21(K11((Domains_of X),(Domains_of X)), Domains_of X) Element of K10(K11(K11((Domains_of X),(Domains_of X)),(Domains_of X)))
LattStr(# (Domains_of X),(Domains_Union X),(Domains_Meet X) #) is strict LattStr
the carrier of (Domains_Lattice X) is non empty set
(Int A) ` is closed Element of K10( the carrier of X)
the carrier of X \ (Int A) is set
Int ((Int A) `) is open Element of K10( the carrier of X)
A ` is Element of K10( the carrier of X)
the carrier of X \ A is set
Cl (A `) is closed Element of K10( the carrier of X)
Int (Cl (A `)) is open Element of K10( the carrier of X)
((Cl (Int A)) `) ` is closed Element of K10( the carrier of X)
the carrier of X \ ((Cl (Int A)) `) is set
(Int (Cl A)) \/ ({} X) is open Element of K10( the carrier of X)
(Int (Cl A)) \/ ((Cl (Int A)) `) is open Element of K10( the carrier of X)
Cl ((Int (Cl A)) \/ ((Cl (Int A)) `)) is closed Element of K10( the carrier of X)
Cl ((Cl (Int A)) `) is closed Element of K10( the carrier of X)
(Cl (Int (Cl A))) \/ (Cl ((Cl (Int A)) `)) is closed Element of K10( the carrier of X)
(Cl A) \/ (Cl (A `)) is closed Element of K10( the carrier of X)
Int ((Cl A) \/ (Cl (A `))) is open Element of K10( the carrier of X)
Cl (Int ((Cl A) \/ (Cl (A `)))) is closed Element of K10( the carrier of X)
A \/ (A `) is Element of K10( the carrier of X)
Cl (A \/ (A `)) is closed Element of K10( the carrier of X)
Int (Cl (A \/ (A `))) is open Element of K10( the carrier of X)
Cl (Int (Cl (A \/ (A `)))) is closed 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)
Cl ([#] X) is closed Element of K10( the carrier of X)
Int (Cl ([#] X)) is open Element of K10( the carrier of X)
Cl (Int (Cl ([#] X))) is closed Element of K10( the carrier of X)
Int ([#] X) is open Element of K10( the carrier of X)
Cl (Int ([#] X)) is closed Element of K10( the carrier of X)
a is Element of the carrier of (Domains_Lattice X)
b is Element of the carrier of (Domains_Lattice X)
a "\/" b is Element of the carrier of (Domains_Lattice X)
(Int ([#] X)) \/ ((Int (Cl A)) \/ ((Cl (Int A)) `)) is open Element of K10( the carrier of X)
([#] X) \/ ((Int (Cl A)) \/ ((Cl (Int A)) `)) is non empty open Element of K10( the carrier of X)
c is Element of the carrier of (Domains_Lattice X)
(a "\/" b) "/\" c is Element of the carrier of (Domains_Lattice X)
([#] X) /\ (Cl (Int A)) is closed Element of K10( the carrier of X)
Int (([#] X) /\ (Cl (Int A))) is open Element of K10( the carrier of X)
Cl (Int (([#] X) /\ (Cl (Int A)))) is closed Element of K10( the carrier of X)
(Cl (Int (([#] X) /\ (Cl (Int A))))) /\ (([#] X) /\ (Cl (Int A))) is closed Element of K10( the carrier of X)
(Cl (Int (Cl (Int A)))) /\ (([#] X) /\ (Cl (Int A))) is closed Element of K10( the carrier of X)
(Cl (Int (Cl (Int A)))) /\ (Cl (Int A)) is closed Element of K10( the carrier of X)
b "/\" c is Element of the carrier of (Domains_Lattice X)
Int (((Cl (Int A)) `) /\ (Cl (Int A))) is open Element of K10( the carrier of X)
Cl (Int (((Cl (Int A)) `) /\ (Cl (Int A)))) is closed Element of K10( the carrier of X)
(Cl (Int (((Cl (Int A)) `) /\ (Cl (Int A))))) /\ (((Cl (Int A)) `) /\ (Cl (Int A))) is Element of K10( the carrier of X)
a "\/" (b "/\" c) is Element of the carrier of (Domains_Lattice X)
(Int (Cl (Int (Cl A)))) \/ (Int (Cl A)) is open Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented LattStr
Closed_Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean LattStr
X is non empty TopSpace-like TopStruct
Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented LattStr
Open_Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean LattStr
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)
{ b1 where b1 is Element of K10( the carrier of X) : b1 is open_condensed } is set
{ b1 where b1 is Element of K10( the carrier of X) : b1 is closed_condensed } is set
A is Element of K10( the carrier of X)
{ b1 where b1 is Element of K10( the carrier of X) : b1 is closed_condensed } is set
{ b1 where b1 is Element of K10( the carrier of X) : b1 is open_condensed } is set
A is Element of K10( the carrier of X)
X is non empty TopSpace-like TopStruct
Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V112() complemented LattStr
Open_Domains_Lattice X is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V112() complemented Boolean LattStr