:: TDLAT_2 semantic presentation

K42() is V35() V36() V37() V41() set

K46() is V35() V36() V37() V38() V39() V40() V41() Element of K10(K42())

K10(K42()) is non empty set

K41() is V35() V36() V37() V38() V39() V40() V41() set

K10(K41()) is non empty set

K10(K46()) is non empty set

1 is non empty ext-real V16() V17() V35() V36() V37() V38() V39() V40() V89() Element of K46()

K11(1,1) is non empty Relation-like set

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

K11(K11(1,1),1) is non empty Relation-like set

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

K11(K11(1,1),K42()) is Relation-like set

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

K11(K42(),K42()) is Relation-like set

K11(K11(K42(),K42()),K42()) is Relation-like set

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

2 is non empty ext-real V16() V17() V35() V36() V37() V38() V39() V40() V89() Element of K46()

K11(2,2) is non empty Relation-like set

K11(K11(2,2),K42()) is Relation-like set

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

{} is empty Relation-like non-empty empty-yielding functional V35() V36() V37() V38() V39() V40() V41() FinSequence-like FinSequence-membered set

3 is non empty ext-real V16() V17() V35() V36() V37() V38() V39() V40() V89() Element of K46()

meet {} is set

Seg 1 is non empty V35() V36() V37() V38() V39() V40() finite V49(1) Element of K10(K46())

{1} is non empty V35() V36() V37() V38() V39() V40() set

Seg 2 is non empty V35() V36() V37() V38() V39() V40() finite V49(2) Element of K10(K46())

{1,2} is non empty V35() V36() V37() V38() V39() V40() set

0 is empty ext-real V16() V17() Relation-like non-empty empty-yielding functional V35() V36() V37() V38() V39() V40() V41() FinSequence-like FinSequence-membered V89() Element of K46()

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

Int F is open Element of K10( the carrier of T)

Cl (Int F) is closed Element of K10( the carrier of T)

Int (Cl (Int F)) is open Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

Int (Cl F) is open Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

Int F is open Element of K10( the carrier of T)

Cl (Int F) is closed Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

Int (Cl F) is open Element of K10( the carrier of T)

Cl (Int (Cl F)) is closed Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

X is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

F /\ X is Element of K10( the carrier of T)

Int (F /\ X) is open Element of K10( the carrier of T)

Cl (Int (F /\ X)) is closed Element of K10( the carrier of T)

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

F \/ X is Element of K10( the carrier of T)

Cl (F \/ X) is closed Element of K10( the carrier of T)

Int (Cl (F \/ X)) is open Element of K10( the carrier of T)

Int F is open Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

Int F is open Element of K10( the carrier of T)

Cl (Int F) is closed Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

Int (Cl F) is open Element of K10( the carrier of T)

F \/ (Int (Cl F)) is Element of K10( the carrier of T)

Int (F \/ (Int (Cl F))) is open Element of K10( the carrier of T)

Cl (Int (F \/ (Int (Cl F)))) is closed Element of K10( the carrier of T)

Cl (Int (Cl F)) is closed Element of K10( the carrier of T)

(Cl (Int (Cl F))) \/ (Cl (Int (Cl F))) is closed Element of K10( the carrier of T)

(Int F) \/ (Int (Cl F)) is open Element of K10( the carrier of T)

Cl ((Int F) \/ (Int (Cl F))) is closed Element of K10( the carrier of T)

Int (Int (Cl F)) is open Element of K10( the carrier of T)

(Int F) \/ (Int (Int (Cl F))) is open Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

Int (Cl F) is open Element of K10( the carrier of T)

Int F is open Element of K10( the carrier of T)

Cl (Int F) is closed Element of K10( the carrier of T)

F /\ (Cl (Int F)) is Element of K10( the carrier of T)

Cl (F /\ (Cl (Int F))) is closed Element of K10( the carrier of T)

Int (Cl (F /\ (Cl (Int F)))) is open Element of K10( the carrier of T)

Int (Cl (Int F)) is open Element of K10( the carrier of T)

(Int (Cl (Int F))) /\ (Int (Cl (Int F))) is open Element of K10( the carrier of T)

(Cl F) /\ (Cl (Int F)) is closed Element of K10( the carrier of T)

Int ((Cl F) /\ (Cl (Int F))) is open Element of K10( the carrier of T)

Cl (Cl (Int F)) is closed Element of K10( the carrier of T)

(Cl F) /\ (Cl (Cl (Int F))) is closed Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

{ b

( b

A is set

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

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

A is Element of K10(K10( the carrier of T))

a is Element of K10(K10( the carrier of T))

b is set

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Cl C1 is closed Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

clf (clf F) is Element of K10(K10( the carrier of T))

{ b

( b

{ b

( b

X is set

A is Element of K10( the carrier of T)

a is Element of K10( the carrier of T)

Cl a is closed Element of K10( the carrier of T)

Cl (Cl a) is closed Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

a is Element of K10( the carrier of T)

Cl a is closed Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

the Element of F is Element of F

A is Element of K10( the carrier of T)

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

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

F /\ X is Element of K10(K10( the carrier of T))

clf (F /\ X) is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

clf X is Element of K10(K10( the carrier of T))

(clf F) /\ (clf X) is Element of K10(K10( the carrier of T))

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

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

clf X is Element of K10(K10( the carrier of T))

(clf F) \ (clf X) is Element of K10(K10( the carrier of T))

F \ X is Element of K10(K10( the carrier of T))

clf (F \ X) is Element of K10(K10( the carrier of T))

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

meet (clf F) is Element of K10( the carrier of T)

union (clf F) is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

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

{ b

( b

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

clf F is Element of K10(K10( the carrier of T))

meet (clf F) is Element of K10( the carrier of T)

X is set

A is Element of K10( the carrier of T)

a is Element of K10( the carrier of T)

Cl a is closed Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Cl (meet F) is closed Element of K10( the carrier of T)

clf F is Element of K10(K10( the carrier of T))

meet (clf F) is Element of K10( the carrier of T)

Cl (meet (clf F)) is closed Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

union (clf F) is Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

X is set

A is Element of K10( the carrier of T)

a is Element of K10( the carrier of T)

Cl a is closed Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

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

A is Element of K10(K10( the carrier of T))

a is set

b is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

a is set

b is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

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

A is Element of K10(K10( the carrier of T))

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

B is open Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

{ b

( b

A is set

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

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

A is Element of K10(K10( the carrier of T))

a is Element of K10(K10( the carrier of T))

b is set

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Int C1 is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

the Element of (T,F) is Element of (T,F)

A is Element of K10( the carrier of T)

a is Element of K10( the carrier of T)

Int a is open Element of K10( the carrier of T)

the Element of F is Element of F

A is Element of K10( the carrier of T)

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

a is set

b is set

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10( the carrier of T)

{F} is non empty set

Int F is open Element of K10( the carrier of T)

{(Int F)} is non empty set

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

(T,X) is Element of K10(K10( the carrier of T))

A is set

a is set

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

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

(T,F) is Element of K10(K10( the carrier of T))

(T,X) is Element of K10(K10( the carrier of T))

b is set

A is set

B is Element of K10( the carrier of T)

a is set

C is Element of K10( the carrier of T)

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

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

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

F \/ X is Element of K10(K10( the carrier of T))

(T,(F \/ X)) is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

(T,X) is Element of K10(K10( the carrier of T))

(T,F) \/ (T,X) is Element of K10(K10( the carrier of T))

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

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

F /\ X is Element of K10(K10( the carrier of T))

(T,(F /\ X)) is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

(T,X) is Element of K10(K10( the carrier of T))

(T,F) /\ (T,X) is Element of K10(K10( the carrier of T))

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

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

(T,X) is Element of K10(K10( the carrier of T))

(T,F) \ (T,X) is Element of K10(K10( the carrier of T))

F \ X is Element of K10(K10( the carrier of T))

(T,(F \ X)) is Element of K10(K10( the carrier of T))

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

union (T,F) is Element of K10( the carrier of T)

meet (T,F) is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

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

{ b

( b

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

union (T,F) is Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

B is set

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

meet (T,F) is Element of K10( the carrier of T)

meet F is Element of K10( the carrier of T)

X is set

A is Element of K10( the carrier of T)

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

{ b

( b

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

union (T,F) is Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

Int (union F) is open Element of K10( the carrier of T)

Int (union (T,F)) is open Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

(T,F) is Element of K10(K10( the carrier of T))

meet (T,F) is Element of K10( the carrier of T)

X is set

A is Element of K10( the carrier of T)

{ b

( b

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

{} T is empty Relation-like non-empty empty-yielding functional V35() V36() V37() V38() V39() V40() V41() FinSequence-like FinSequence-membered open closed boundary nowhere_dense Element of K10( the carrier of T)

T is TopSpace-like TopStruct

the carrier of T is set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

(T,F) is Element of K10(K10( the carrier of T))

meet (T,F) is Element of K10( the carrier of T)

X is Relation-like K46() -defined Function-like finite FinSequence-like FinSubsequence-like set

rng X is set

dom X is V35() V36() V37() V38() V39() V40() Element of K10(K46())

A is ext-real V16() V17() V89() set

Seg A is V35() V36() V37() V38() V39() V40() finite V49(A) Element of K10(K46())

a is ext-real V16() V17() V89() set

Seg a is V35() V36() V37() V38() V39() V40() finite V49(a) Element of K10(K46())

X .: (Seg a) is set

a + 1 is ext-real V16() V17() V35() V36() V37() V38() V39() V40() V89() Element of K46()

Seg (a + 1) is V35() V36() V37() V38() V39() V40() finite V49(a + 1) Element of K10(K46())

X .: (Seg (a + 1)) is set

b is Element of K10(K10( the carrier of T))

(T,b) is Element of K10(K10( the carrier of T))

meet (T,b) is Element of K10( the carrier of T)

meet b is Element of K10( the carrier of T)

Int (meet b) is open Element of K10( the carrier of T)

Im (X,(a + 1)) is set

{(a + 1)} is non empty V35() V36() V37() V38() V39() V40() set

X .: {(a + 1)} is set

0 + 1 is ext-real V16() V17() V35() V36() V37() V38() V39() V40() V89() Element of K46()

B is Element of K10(K10( the carrier of T))

X . (a + 1) is set

{(X . (a + 1))} is non empty set

meet B is Element of K10( the carrier of T)

(T,B) is Element of K10(K10( the carrier of T))

meet (T,B) is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Int C1 is open Element of K10( the carrier of T)

{(Int C1)} is non empty set

meet {(Int C1)} is set

Int (meet B) is open Element of K10( the carrier of T)

A + 1 is ext-real V16() V17() V35() V36() V37() V38() V39() V40() V89() Element of K46()

C is Element of K10(K10( the carrier of T))

(T,C) is Element of K10(K10( the carrier of T))

meet (T,C) is Element of K10( the carrier of T)

meet C is Element of K10( the carrier of T)

Int (meet C) is open Element of K10( the carrier of T)

X . a is set

(Seg a) \/ {(a + 1)} is non empty V35() V36() V37() V38() V39() V40() set

X .: ((Seg a) \/ {(a + 1)}) is set

(X .: (Seg a)) \/ (X .: {(a + 1)}) is set

(meet C) /\ (meet B) is Element of K10( the carrier of T)

Int ((meet C) /\ (meet B)) is open Element of K10( the carrier of T)

(Int (meet C)) /\ (Int (meet B)) is open Element of K10( the carrier of T)

(meet (T,C)) /\ (meet (T,B)) is Element of K10( the carrier of T)

(T,C) \/ (T,B) is Element of K10(K10( the carrier of T))

meet ((T,C) \/ (T,B)) is Element of K10( the carrier of T)

Im (X,1) is set

X .: {1} is set

X . 1 is set

{(X . 1)} is non empty set

union b is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

{(Int B)} is non empty set

meet {(Int B)} is set

Seg 0 is empty Relation-like non-empty empty-yielding functional V35() V36() V37() V38() V39() V40() V41() finite V49( 0 ) FinSequence-like FinSequence-membered Element of K10(K46())

X .: (Seg 0) is empty Relation-like non-empty empty-yielding functional V35() V36() V37() V38() V39() V40() V41() FinSequence-like FinSequence-membered set

a is Element of K10(K10( the carrier of T))

(T,a) is Element of K10(K10( the carrier of T))

meet (T,a) is Element of K10( the carrier of T)

meet a is Element of K10( the carrier of T)

Int (meet a) is open Element of K10( the carrier of T)

X .: (Seg A) is set

0 + 1 is ext-real V16() V17() V35() V36() V37() V38() V39() V40() V89() Element of K46()

X .: {} is empty Relation-like non-empty empty-yielding functional V35() V36() V37() V38() V39() V40() V41() FinSequence-like FinSequence-membered set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

{ b

( b

A is set

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

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

Cl (Int b) is closed Element of K10( the carrier of T)

A is Element of K10(K10( the carrier of T))

a is Element of K10(K10( the carrier of T))

b is set

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Int C1 is open Element of K10( the carrier of T)

Cl (Int C1) is closed Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Cl (Int C) is closed Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

C1 is Element of K10( the carrier of T)

Int C1 is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

{ b

( b

A is set

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

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

Int (Cl b) is open Element of K10( the carrier of T)

A is Element of K10(K10( the carrier of T))

a is Element of K10(K10( the carrier of T))

b is set

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Cl C1 is closed Element of K10( the carrier of T)

Int (Cl C1) is open Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Int (Cl C) is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

C1 is Element of K10( the carrier of T)

Cl C1 is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

{ b

( b

A is set

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

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

Int (Cl b) is open Element of K10( the carrier of T)

Cl (Int (Cl b)) is closed Element of K10( the carrier of T)

A is Element of K10(K10( the carrier of T))

a is Element of K10(K10( the carrier of T))

b is set

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Cl C1 is closed Element of K10( the carrier of T)

Int (Cl C1) is open Element of K10( the carrier of T)

Cl (Int (Cl C1)) is closed Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Int (Cl C) is open Element of K10( the carrier of T)

Cl (Int (Cl C)) is closed Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

C1 is Element of K10( the carrier of T)

Int C1 is open Element of K10( the carrier of T)

c is Element of K10( the carrier of T)

Cl c is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

{ b

( b

A is set

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

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

Cl (Int b) is closed Element of K10( the carrier of T)

Int (Cl (Int b)) is open Element of K10( the carrier of T)

A is Element of K10(K10( the carrier of T))

a is Element of K10(K10( the carrier of T))

b is set

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Int C1 is open Element of K10( the carrier of T)

Cl (Int C1) is closed Element of K10( the carrier of T)

Int (Cl (Int C1)) is open Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Cl (Int C) is closed Element of K10( the carrier of T)

Int (Cl (Int C)) is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

C1 is Element of K10( the carrier of T)

Cl C1 is closed Element of K10( the carrier of T)

c is Element of K10( the carrier of T)

Int c is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

clf (T,(clf (T,F))) is Element of K10(K10( the carrier of T))

{ b

( b

A is Element of K10(K10( the carrier of T))

clf A is Element of K10(K10( the carrier of T))

{ b

( b

a is set

b is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Cl (Int C) is closed Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

Cl (Int B) is closed Element of K10( the carrier of T)

Int (Cl (Int B)) is open Element of K10( the carrier of T)

Cl (Int (Cl (Int B))) is closed Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Int C1 is open Element of K10( the carrier of T)

Cl (Int C1) is closed Element of K10( the carrier of T)

Int (Cl (Int C1)) is open Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Cl (Int C) is closed Element of K10( the carrier of T)

Int (Cl (Int C)) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

(T,(clf (T,(clf F)))) is Element of K10(K10( the carrier of T))

{ b

( b

A is Element of K10(K10( the carrier of T))

(T,A) is Element of K10(K10( the carrier of T))

{ b

( b

a is set

b is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Int (Cl C) is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

Int (Cl B) is open Element of K10( the carrier of T)

Cl (Int (Cl B)) is closed Element of K10( the carrier of T)

Int (Cl (Int (Cl B))) is open Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

C1 is Element of K10( the carrier of T)

Cl C1 is closed Element of K10( the carrier of T)

Int (Cl C1) is open Element of K10( the carrier of T)

Cl (Int (Cl C1)) is closed Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Int (Cl C) is open Element of K10( the carrier of T)

Cl (Int (Cl C)) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

union (T,(clf F)) is Element of K10( the carrier of T)

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

union (clf (T,(clf F))) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

Int (Cl B) is open Element of K10( the carrier of T)

Cl (Int (Cl B)) is closed Element of K10( the carrier of T)

C is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

meet (T,(clf F)) is Element of K10( the carrier of T)

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

meet (clf (T,(clf F))) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

union (clf (T,F)) is Element of K10( the carrier of T)

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

union (clf (T,(clf F))) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

Int (Cl B) is open Element of K10( the carrier of T)

Cl (Int (Cl B)) is closed Element of K10( the carrier of T)

C is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

meet (clf (T,F)) is Element of K10( the carrier of T)

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

meet (clf (T,(clf F))) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

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

Cl (Int C) is closed Element of K10( the carrier of T)

Int (Cl C) is open Element of K10( the carrier of T)

Cl (Int (Cl C)) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

union (T,(clf (T,F))) is Element of K10( the carrier of T)

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

union (T,(clf F)) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

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

Int (Cl C) is open Element of K10( the carrier of T)

C1 is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

meet (T,(clf (T,F))) is Element of K10( the carrier of T)

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

meet (T,(clf F)) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

Cl (Int B) is closed Element of K10( the carrier of T)

Int (Cl (Int B)) is open Element of K10( the carrier of T)

Int (Cl B) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

union (T,(clf (T,F))) is Element of K10( the carrier of T)

union (clf (T,F)) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Cl (Int C) is closed Element of K10( the carrier of T)

C1 is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

meet (T,(clf (T,F))) is Element of K10( the carrier of T)

meet (clf (T,F)) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

Cl (Int B) is closed Element of K10( the carrier of T)

Int (Cl (Int B)) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

union (clf (T,(clf F))) is Element of K10( the carrier of T)

union (clf F) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Int B is open Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

C1 is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

meet (clf (T,(clf F))) is Element of K10( the carrier of T)

meet (clf F) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Cl b is closed Element of K10( the carrier of T)

Int (Cl b) is open Element of K10( the carrier of T)

Cl (Int (Cl b)) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

union (T,F) is Element of K10( the carrier of T)

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

union (T,(clf (T,F))) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

Cl (Int b) is closed Element of K10( the carrier of T)

Int (Cl (Int b)) is open Element of K10( the carrier of T)

B is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

meet (T,F) is Element of K10( the carrier of T)

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

meet (T,(clf (T,F))) is Element of K10( the carrier of T)

X is set

A is set

a is Element of K10( the carrier of T)

b is Element of K10( the carrier of T)

Int b is open Element of K10( the carrier of T)

B is Element of K10( the carrier of T)

Cl B is closed Element of K10( the carrier of T)

C is Element of K10( the carrier of T)

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

Cl (Int C) is closed Element of K10( the carrier of T)

Int (Cl (Int C)) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

union (clf (T,F)) is Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

Int (union F) is open Element of K10( the carrier of T)

Cl (Int (union F)) is closed Element of K10( the carrier of T)

union (T,F) is Element of K10( the carrier of T)

Cl (union (T,F)) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

Cl (Int (meet F)) is closed Element of K10( the carrier of T)

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

meet (clf (T,F)) is Element of K10( the carrier of T)

meet (T,F) is Element of K10( the carrier of T)

Cl (meet (T,F)) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

union (T,(clf F)) is Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

Int (Cl (union F)) is open Element of K10( the carrier of T)

union (clf F) is Element of K10( the carrier of T)

Int (union (clf F)) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Cl (meet F) is closed Element of K10( the carrier of T)

Int (Cl (meet F)) is open Element of K10( the carrier of T)

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

meet (T,(clf F)) is Element of K10( the carrier of T)

meet (clf F) is Element of K10( the carrier of T)

Int (meet (clf F)) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

union (clf (T,(clf F))) is Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

Int (Cl (union F)) is open Element of K10( the carrier of T)

Cl (Int (Cl (union F))) is closed Element of K10( the carrier of T)

union (T,(clf F)) is Element of K10( the carrier of T)

Cl (union (T,(clf F))) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Cl (meet F) is closed Element of K10( the carrier of T)

Int (Cl (meet F)) is open Element of K10( the carrier of T)

Cl (Int (Cl (meet F))) is closed Element of K10( the carrier of T)

clf F is Element of K10(K10( the carrier of T))

(T,(clf F)) is Element of K10(K10( the carrier of T))

clf (T,(clf F)) is Element of K10(K10( the carrier of T))

meet (clf (T,(clf F))) is Element of K10( the carrier of T)

meet (T,(clf F)) is Element of K10( the carrier of T)

Cl (meet (T,(clf F))) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

union (T,(clf (T,F))) is Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

Int (union F) is open Element of K10( the carrier of T)

Cl (Int (union F)) is closed Element of K10( the carrier of T)

Int (Cl (Int (union F))) is open Element of K10( the carrier of T)

union (clf (T,F)) is Element of K10( the carrier of T)

Int (union (clf (T,F))) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

Cl (Int (meet F)) is closed Element of K10( the carrier of T)

Int (Cl (Int (meet F))) is open Element of K10( the carrier of T)

(T,F) is Element of K10(K10( the carrier of T))

clf (T,F) is Element of K10(K10( the carrier of T))

(T,(clf (T,F))) is Element of K10(K10( the carrier of T))

meet (T,(clf (T,F))) is Element of K10( the carrier of T)

meet (clf (T,F)) is Element of K10( the carrier of T)

Int (meet (clf (T,F))) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

Int (union F) is open Element of K10( the carrier of T)

Cl (Int (union F)) is closed Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

Int (Cl (union F)) is open Element of K10( the carrier of T)

Cl (Int (Cl (union F))) is closed Element of K10( the carrier of T)

Cl (Cl (union F)) is closed Element of K10( the carrier of T)

X is set

A is Element of K10( the carrier of T)

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

Cl (Int A) is closed Element of K10( the carrier of T)

Cl (Cl (Int (union F))) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Cl (meet F) is closed Element of K10( the carrier of T)

Int (Cl (meet F)) is open Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

Cl (Int (meet F)) is closed Element of K10( the carrier of T)

Int (Cl (Int (meet F))) is open Element of K10( the carrier of T)

Int (Int (meet F)) is open Element of K10( the carrier of T)

{} T is empty proper Relation-like non-empty empty-yielding functional V35() V36() V37() V38() V39() V40() V41() FinSequence-like FinSequence-membered open closed boundary nowhere_dense Element of K10( the carrier of T)

Cl ({} T) is closed Element of K10( the carrier of T)

X is set

A is Element of K10( the carrier of T)

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

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

Int (Int (Cl (meet F))) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

X is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

F \/ X is Element of K10( the carrier of T)

Cl (F \/ X) is closed Element of K10( the carrier of T)

Int (Cl (F \/ X)) is open Element of K10( the carrier of T)

(Int (Cl (F \/ X))) \/ (F \/ X) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

F /\ X is Element of K10( the carrier of T)

Int (F /\ X) is open Element of K10( the carrier of T)

Cl (Int (F /\ X)) is closed Element of K10( the carrier of T)

(Cl (Int (F /\ X))) /\ (F /\ X) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

Int F is open Element of K10( the carrier of T)

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

Cl (Int F) is closed Element of K10( the carrier of T)

Cl (Int X) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

Cl F is closed Element of K10( the carrier of T)

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

Int (Cl F) is open Element of K10( the carrier of T)

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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

F is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

F /\ X is Element of K10( the carrier of T)

Int (F /\ X) is open Element of K10( the carrier of T)

Cl (Int (F /\ X)) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

X is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

F \/ X is Element of K10( the carrier of T)

Cl (F \/ X) is closed Element of K10( the carrier of T)

Int (Cl (F \/ X)) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

Domains_of T is non empty Element of K10(K10( the carrier of T))

F is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

{ b

A is Element of K10( the carrier of T)

X is set

A is Element of K10( the carrier of T)

{ b

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

Int (union F) is open Element of K10( the carrier of T)

Cl (Int (union F)) is closed Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

Int (Cl (union F)) is open Element of K10( the carrier of T)

Cl (Int (Cl (union F))) is closed Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

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

Cl (Int X) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Cl (meet F) is closed Element of K10( the carrier of T)

Int (Cl (meet F)) is open Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

Cl (Int (meet F)) is closed Element of K10( the carrier of T)

Int (Cl (Int (meet F))) is open Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

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

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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

Int (Cl (union F)) is open Element of K10( the carrier of T)

(union F) \/ (Int (Cl (union F))) is Element of K10( the carrier of T)

Cl (Int (Cl (union F))) is closed Element of K10( the carrier of T)

Cl (Cl (union F)) is closed Element of K10( the carrier of T)

Int (union F) is open Element of K10( the carrier of T)

Cl (Int (union F)) is closed Element of K10( the carrier of T)

Int ((union F) \/ (Int (Cl (union F)))) is open Element of K10( the carrier of T)

Cl (Int ((union F) \/ (Int (Cl (union F))))) is closed Element of K10( the carrier of T)

Cl ((union F) \/ (Int (Cl (union F)))) is closed Element of K10( the carrier of T)

Int (Cl ((union F) \/ (Int (Cl (union F))))) is open Element of K10( the carrier of T)

(Cl (union F)) \/ (Cl (Int (Cl (union F)))) is closed Element of K10( the carrier of T)

Int ((Cl (union F)) \/ (Cl (Int (Cl (union F))))) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

Int (Cl (union F)) is open Element of K10( the carrier of T)

(union F) \/ (Int (Cl (union F))) is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

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

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

A is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

Cl (Int (meet F)) is closed Element of K10( the carrier of T)

(meet F) /\ (Cl (Int (meet F))) is Element of K10( the carrier of T)

Int (Int (meet F)) is open Element of K10( the carrier of T)

Int (Cl (Int (meet F))) is open Element of K10( the carrier of T)

Cl (meet F) is closed Element of K10( the carrier of T)

Int (Cl (meet F)) is open Element of K10( the carrier of T)

Cl ((meet F) /\ (Cl (Int (meet F)))) is closed Element of K10( the carrier of T)

Int (Cl ((meet F) /\ (Cl (Int (meet F))))) is open Element of K10( the carrier of T)

Int ((meet F) /\ (Cl (Int (meet F)))) is open Element of K10( the carrier of T)

Cl (Int ((meet F) /\ (Cl (Int (meet F))))) is closed Element of K10( the carrier of T)

(Int (meet F)) /\ (Int (Cl (Int (meet F)))) is open Element of K10( the carrier of T)

Cl ((Int (meet F)) /\ (Int (Cl (Int (meet F))))) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

Cl (Int (meet F)) is closed Element of K10( the carrier of T)

(meet F) /\ (Cl (Int (meet F))) is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

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

Cl (Int X) is closed Element of K10( the carrier of T)

A is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

Closed_Domains_of T is non empty Element of K10(K10( the carrier of T))

F is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

{ b

A is Element of K10( the carrier of T)

X is set

A is Element of K10( the carrier of T)

{ b

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

Closed_Domains_of T is non empty Element of K10(K10( the carrier of T))

Domains_of T is non empty Element of K10(K10( the carrier of T))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

clf F is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

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

a is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

Cl (Int (meet F)) is closed Element of K10( the carrier of T)

Int (Cl (union F)) is open Element of K10( the carrier of T)

Cl (Int (Cl (union F))) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

a is set

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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

Cl (Int (meet F)) is closed Element of K10( the carrier of T)

Cl (meet F) is closed Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

A is set

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

Cl (Int X) is closed Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

Open_Domains_of T is non empty Element of K10(K10( the carrier of T))

F is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

{ b

A is Element of K10( the carrier of T)

X is set

A is Element of K10( the carrier of T)

{ b

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

Open_Domains_of T is non empty Element of K10(K10( the carrier of T))

Domains_of T is non empty Element of K10(K10( the carrier of T))

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

(T,F) is Element of K10(K10( the carrier of T))

X is Element of K10( the carrier of T)

A is Element of K10( the carrier of T)

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

a is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

union F is Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

Int (Cl (union F)) is open Element of K10( the carrier of T)

Cl (Int (meet F)) is closed Element of K10( the carrier of T)

Int (Cl (Int (meet F))) is open Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

union F is Element of K10( the carrier of T)

Cl (union F) is closed Element of K10( the carrier of T)

Int (Cl (union F)) is open Element of K10( the carrier of T)

Int (union F) is open Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

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

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

A is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

F is Element of K10(K10( the carrier of T))

meet F is Element of K10( the carrier of T)

Int (meet F) is open Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

X is Element of K10( the carrier of T)

A is set

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

T is non empty TopSpace-like TopStruct

Domains_Lattice T is non empty Lattice-like V131() complemented LattStr

the carrier of (Domains_Lattice T) is non empty set

Domains_of T is non empty Element of K10(K10( the carrier of T))

the carrier of T is non empty set

K10( the carrier of T) is non empty set

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

Domains_Union T is Relation-like Function-like V32(K11((Domains_of T),(Domains_of T)), Domains_of T) Element of K10(K11(K11((Domains_of T),(Domains_of T)),(Domains_of T)))

K11((Domains_of T),(Domains_of T)) is non empty Relation-like set

K11(K11((Domains_of T),(Domains_of T)),(Domains_of T)) is non empty Relation-like set

K10(K11(K11((Domains_of T),(Domains_of T)),(Domains_of T))) is non empty set

Domains_Meet T is Relation-like Function-like V32(K11((Domains_of T),(Domains_of T)), Domains_of T) Element of K10(K11(K11((Domains_of T),(Domains_of T)),(Domains_of T)))

LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #) is strict LattStr

T is non empty TopSpace-like TopStruct

Domains_Lattice T is non empty Lattice-like V131() complemented LattStr

the carrier of (Domains_Lattice T) is non empty set

the carrier of T is non empty set

K10( the