:: TDLAT_3 semantic presentation

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)

{ b

( b

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)

{ b

( b

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)

{ b

C is Element of K10( the carrier of X)

{ b

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)

{ b

C is Element of K10( the carrier of X)

{ b

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)

{ b

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)

{ b

{ b

A is Element of K10( the carrier of X)

{ b

{ b

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