:: 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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Cl b₂ & b₂ in F ) } is set
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Cl b₂ & b₂ in clf F ) } is set
{ b₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Cl b₂ & b₂ in F ) } is set
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Cl b₂ & b₂ in F ) } 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))
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Int b₂ & b₂ in F ) } is set
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Int b₂ & b₂ in F ) } 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))
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Int b₂ & b₂ in F ) } 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))
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Int b₂ & b₂ in F ) } 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 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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Cl (Int b₂) & b₂ in F ) } is set
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Int (Cl b₂) & b₂ in F ) } is set
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Cl (Int (Cl b₂)) & b₂ in F ) } is set
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Int (Cl (Int b₂)) & b₂ in F ) } is set
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Int (Cl (Int b₂)) & b₂ in F ) } is set
A is Element of K10(K10( the carrier of T))
clf A is Element of K10(K10( the carrier of T))
{ b₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Cl (Int b₂) & b₂ in F ) } is set
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₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Cl (Int (Cl b₂)) & b₂ in F ) } is set
A is Element of K10(K10( the carrier of T))
(T,A) is Element of K10(K10( the carrier of T))
{ b₁ where b₁ is Element of K10( the carrier of T) : ex b₂ being Element of K10( the carrier of T) st
( b₁ = Int (Cl b₂) & b₂ in F ) } is set
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₁ where b₁ is Element of K10( the carrier of T) : b₁ is condensed } is set
A is Element of K10( the carrier of T)
X is set
A is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is condensed } 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))
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₁ where b₁ is Element of K10( the carrier of T) : b₁ is closed_condensed } is set
A is Element of K10( the carrier of T)
X is set
A is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is closed_condensed } 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))
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₁ where b₁ is Element of K10( the carrier of T) : b₁ is open_condensed } is set
A is Element of K10( the carrier of T)
X is set
A is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is open_condensed } 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))
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 carrier of T) is non empty set
Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
F is Element of the carrier of (Domains_Lattice T)
X is Element of the carrier of (Domains_Lattice T)
F "\/" X is Element of the carrier of (Domains_Lattice T)
F "/\" X is Element of the carrier of (Domains_Lattice T)
A is Element of Domains_of T
a is Element of Domains_of T
A \/ a is Element of K10( the carrier of T)
Cl (A \/ a) is closed Element of K10( the carrier of T)
Int (Cl (A \/ a)) is open Element of K10( the carrier of T)
(Int (Cl (A \/ a))) \/ (A \/ a) is Element of K10( the carrier of T)
A /\ a is Element of K10( the carrier of T)
Int (A /\ a) is open Element of K10( the carrier of T)
Cl (Int (A /\ a)) is closed Element of K10( the carrier of T)
(Cl (Int (A /\ a))) /\ (A /\ a) is Element of K10( the carrier of T)
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
(Domains_Union T) . (A,a) is Element of Domains_of T
(Domains_Meet T) . (A,a) is Element of Domains_of T
T is non empty TopSpace-like TopStruct
Domains_Lattice T is non empty Lattice-like V131() complemented LattStr
Bottom (Domains_Lattice T) is Element of the carrier of (Domains_Lattice T)
the carrier of (Domains_Lattice T) is non empty set
{} 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)
the carrier of T is non empty set
K10( the carrier of T) is non empty set
Top (Domains_Lattice T) is Element of the carrier of (Domains_Lattice T)
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is condensed } is set
Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
X is Element of the carrier of (Domains_Lattice T)
A is Element of the carrier of (Domains_Lattice T)
X "\/" A is Element of the carrier of (Domains_Lattice T)
a is Element of Domains_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)
b is Element of K10( the carrier of T)
F is Element of Domains_of T
F \/ a is Element of K10( the carrier of T)
Cl (F \/ a) is closed Element of K10( the carrier of T)
Int (Cl (F \/ a)) is open Element of K10( the carrier of T)
(Int (Cl (F \/ a))) \/ (F \/ a) is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is condensed } is set
Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
X is Element of the carrier of (Domains_Lattice T)
A is Element of the carrier of (Domains_Lattice T)
X "/\" A is Element of the carrier of (Domains_Lattice T)
a is Element of Domains_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)
b is Element of K10( the carrier of T)
F is Element of Domains_of T
F /\ a is Element of K10( the carrier of T)
Int (F /\ a) is open Element of K10( the carrier of T)
Cl (Int (F /\ a)) is closed Element of K10( the carrier of T)
(Cl (Int (F /\ a))) /\ (F /\ a) is Element of K10( the carrier of T)
([#] T) /\ a is Element of K10( the carrier of T)
(Cl (Int a)) /\ (([#] T) /\ a) is Element of K10( the carrier of T)
(Cl (Int a)) /\ a is 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
the carrier of T is non empty set
K10( the carrier of T) is non empty set
Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
F is Element of the carrier of (Domains_Lattice T)
X is Element of the carrier of (Domains_Lattice T)
A is Element of Domains_of T
a is Element of Domains_of T
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is condensed } is set
F "\/" X is Element of the carrier of (Domains_Lattice T)
A \/ a is Element of K10( the carrier of T)
Cl (A \/ a) is closed Element of K10( the carrier of T)
Int (Cl (A \/ a)) is open Element of K10( the carrier of T)
(Int (Cl (A \/ a))) \/ (A \/ a) is Element of K10( the carrier of T)
b is Element of K10( the carrier of T)
A \/ a is Element of K10( the carrier of T)
Cl (A \/ a) is closed Element of K10( the carrier of T)
Int (Cl (A \/ a)) is open Element of K10( the carrier of T)
(Int (Cl (A \/ a))) \/ (A \/ a) is Element of K10( the carrier of T)
b is Element of K10( the carrier of T)
F "\/" X is Element of the carrier of (Domains_Lattice 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
K10( the carrier of (Domains_Lattice T)) is non empty set
F is Element of K10( the carrier of (Domains_Lattice T))
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
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
Cl (union X) is closed Element of K10( the carrier of T)
Int (Cl (union X)) is open Element of K10( the carrier of T)
(union X) \/ (Int (Cl (union X))) is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is condensed } is set
a is Element of the carrier of (Domains_Lattice T)
b is Element of the carrier of (Domains_Lattice T)
B is Element of Domains_of T
C is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
c is Element of the carrier of (Domains_Lattice T)
C is Element of K10( the carrier of T)
b is Element of the carrier of (Domains_Lattice T)
B is Element of Domains_of T
b is Element of the carrier of (Domains_Lattice 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
F is set
{ b₁ where b₁ is Element of the carrier of (Domains_Lattice T) : b₁ in F } is set
A is Element of the carrier of (Domains_Lattice T)
a is Element of the carrier of (Domains_Lattice T)
A is Element of the carrier of (Domains_Lattice T)
a is Element of the carrier of (Domains_Lattice T)
b is Element of the carrier of (Domains_Lattice T)
A is set
a is Element of the carrier of (Domains_Lattice T)
K10( the carrier of (Domains_Lattice T)) is non empty set
A is Element of K10( the carrier of (Domains_Lattice T))
a is Element of the carrier of (Domains_Lattice T)
b is Element of the carrier of (Domains_Lattice T)
b is Element of the carrier of (Domains_Lattice 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
Domains_Lattice T is non empty Lattice-like V131() complemented LattStr
the carrier of (Domains_Lattice T) is non empty set
K10( the carrier of (Domains_Lattice 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 (Domains_Lattice T))
"\/" (X,(Domains_Lattice T)) is Element of the carrier of (Domains_Lattice T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is condensed } is set
Domains_of T is non empty Element of K10(K10( the carrier of T))
a is Element of the carrier of (Domains_Lattice T)
b is Element of the carrier of (Domains_Lattice T)
B is Element of Domains_of T
b is Element of the carrier of (Domains_Lattice T)
B is Element of Domains_of T
C is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
c is Element of the carrier of (Domains_Lattice T)
C 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
Domains_Lattice T is non empty Lattice-like V131() complemented LattStr
the carrier of (Domains_Lattice T) is non empty set
K10( the carrier of (Domains_Lattice T)) is non empty set
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
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 (Domains_Lattice T))
"/\" (X,(Domains_Lattice T)) is Element of the carrier of (Domains_Lattice T)
{ b₁ where b₁ is Element of the carrier of (Domains_Lattice T) : b₁ is_less_than X } is set
"\/" ( { b₁ where b₁ is Element of the carrier of (Domains_Lattice T) : b₁ is_less_than X } ,(Domains_Lattice T)) is Element of the carrier of (Domains_Lattice T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is condensed } is set
Domains_of T is non empty Element of K10(K10( the carrier of T))
a is Element of the carrier of (Domains_Lattice T)
b is Element of the carrier of (Domains_Lattice T)
B is Element of Domains_of T
b is Element of the carrier of (Domains_Lattice T)
B is Element of Domains_of T
C is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
c is Element of the carrier of (Domains_Lattice T)
C is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is condensed } is set
Domains_of T is non empty Element of K10(K10( the carrier of T))
a is Element of the carrier of (Domains_Lattice T)
b is Element of the carrier of (Domains_Lattice T)
B is Element of Domains_of T
b is Element of the carrier of (Domains_Lattice T)
T is non empty TopSpace-like TopStruct
Closed_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Closed_Domains_Lattice T) is non empty set
Closed_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
Closed_Domains_Union T is Relation-like Function-like V32(K11((Closed_Domains_of T),(Closed_Domains_of T)), Closed_Domains_of T) Element of K10(K11(K11((Closed_Domains_of T),(Closed_Domains_of T)),(Closed_Domains_of T)))
K11((Closed_Domains_of T),(Closed_Domains_of T)) is non empty Relation-like set
K11(K11((Closed_Domains_of T),(Closed_Domains_of T)),(Closed_Domains_of T)) is non empty Relation-like set
K10(K11(K11((Closed_Domains_of T),(Closed_Domains_of T)),(Closed_Domains_of T))) is non empty set
Closed_Domains_Meet T is Relation-like Function-like V32(K11((Closed_Domains_of T),(Closed_Domains_of T)), Closed_Domains_of T) Element of K10(K11(K11((Closed_Domains_of T),(Closed_Domains_of T)),(Closed_Domains_of T)))
LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #) is strict LattStr
T is non empty TopSpace-like TopStruct
Closed_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Closed_Domains_Lattice T) is non empty set
the carrier of T is non empty set
K10( the carrier of T) is non empty set
Closed_Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
F is Element of the carrier of (Closed_Domains_Lattice T)
X is Element of the carrier of (Closed_Domains_Lattice T)
F "\/" X is Element of the carrier of (Closed_Domains_Lattice T)
F "/\" X is Element of the carrier of (Closed_Domains_Lattice T)
A is Element of Closed_Domains_of T
a is Element of Closed_Domains_of T
A \/ a is Element of K10( the carrier of T)
A /\ a is Element of K10( the carrier of T)
Int (A /\ a) is open Element of K10( the carrier of T)
Cl (Int (A /\ a)) is closed Element of K10( the carrier of T)
Closed_Domains_Union T is Relation-like Function-like V32(K11((Closed_Domains_of T),(Closed_Domains_of T)), Closed_Domains_of T) Element of K10(K11(K11((Closed_Domains_of T),(Closed_Domains_of T)),(Closed_Domains_of T)))
K11((Closed_Domains_of T),(Closed_Domains_of T)) is non empty Relation-like set
K11(K11((Closed_Domains_of T),(Closed_Domains_of T)),(Closed_Domains_of T)) is non empty Relation-like set
K10(K11(K11((Closed_Domains_of T),(Closed_Domains_of T)),(Closed_Domains_of T))) is non empty set
Closed_Domains_Meet T is Relation-like Function-like V32(K11((Closed_Domains_of T),(Closed_Domains_of T)), Closed_Domains_of T) Element of K10(K11(K11((Closed_Domains_of T),(Closed_Domains_of T)),(Closed_Domains_of T)))
LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #) is strict LattStr
(Closed_Domains_Union T) . (A,a) is Element of Closed_Domains_of T
(Closed_Domains_Meet T) . (A,a) is Element of Closed_Domains_of T
T is non empty TopSpace-like TopStruct
Closed_Domains_Lattice T is non empty Lattice-like Boolean LattStr
Bottom (Closed_Domains_Lattice T) is Element of the carrier of (Closed_Domains_Lattice T)
the carrier of (Closed_Domains_Lattice T) is non empty set
{} 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)
the carrier of T is non empty set
K10( the carrier of T) is non empty set
Top (Closed_Domains_Lattice T) is Element of the carrier of (Closed_Domains_Lattice T)
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is closed_condensed } is set
Closed_Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
X is Element of the carrier of (Closed_Domains_Lattice T)
A is Element of the carrier of (Closed_Domains_Lattice T)
X "\/" A is Element of the carrier of (Closed_Domains_Lattice T)
F is Element of Closed_Domains_of T
a is Element of Closed_Domains_of T
F \/ a is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is closed_condensed } is set
Closed_Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
X is Element of the carrier of (Closed_Domains_Lattice T)
A is Element of the carrier of (Closed_Domains_Lattice T)
X "/\" A is Element of the carrier of (Closed_Domains_Lattice T)
a is Element of Closed_Domains_of T
F is Element of Closed_Domains_of T
F /\ a is Element of K10( the carrier of T)
Int (F /\ a) is open Element of K10( the carrier of T)
Cl (Int (F /\ a)) is closed 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)
b is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
Closed_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Closed_Domains_Lattice T) is non empty set
the carrier of T is non empty set
K10( the carrier of T) is non empty set
Closed_Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
F is Element of the carrier of (Closed_Domains_Lattice T)
X is Element of the carrier of (Closed_Domains_Lattice T)
A is Element of Closed_Domains_of T
a is Element of Closed_Domains_of T
F "\/" X is Element of the carrier of (Closed_Domains_Lattice T)
A \/ a is Element of K10( the carrier of T)
A \/ a is Element of K10( the carrier of T)
F "\/" X is Element of the carrier of (Closed_Domains_Lattice T)
T is non empty TopSpace-like TopStruct
Closed_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Closed_Domains_Lattice T) is non empty set
K10( the carrier of (Closed_Domains_Lattice T)) is non empty set
F is Element of K10( the carrier of (Closed_Domains_Lattice T))
Closed_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
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
Cl (union X) is closed Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is closed_condensed } is set
a is Element of the carrier of (Closed_Domains_Lattice T)
b is Element of the carrier of (Closed_Domains_Lattice T)
B is Element of Closed_Domains_of T
C is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
c is Element of the carrier of (Closed_Domains_Lattice T)
C is Element of K10( the carrier of T)
b is Element of the carrier of (Closed_Domains_Lattice T)
B is Element of Closed_Domains_of T
b is Element of the carrier of (Closed_Domains_Lattice T)
T is non empty TopSpace-like TopStruct
Closed_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Closed_Domains_Lattice T) is non empty set
F is set
{ b₁ where b₁ is Element of the carrier of (Closed_Domains_Lattice T) : b₁ in F } is set
A is Element of the carrier of (Closed_Domains_Lattice T)
a is Element of the carrier of (Closed_Domains_Lattice T)
A is Element of the carrier of (Closed_Domains_Lattice T)
a is Element of the carrier of (Closed_Domains_Lattice T)
b is Element of the carrier of (Closed_Domains_Lattice T)
A is set
a is Element of the carrier of (Closed_Domains_Lattice T)
K10( the carrier of (Closed_Domains_Lattice T)) is non empty set
A is Element of K10( the carrier of (Closed_Domains_Lattice T))
a is Element of the carrier of (Closed_Domains_Lattice T)
b is Element of the carrier of (Closed_Domains_Lattice T)
b is Element of the carrier of (Closed_Domains_Lattice 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
Closed_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Closed_Domains_Lattice T) is non empty set
K10( the carrier of (Closed_Domains_Lattice 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 (Closed_Domains_Lattice T))
"\/" (X,(Closed_Domains_Lattice T)) is Element of the carrier of (Closed_Domains_Lattice T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is closed_condensed } is set
Closed_Domains_of T is non empty Element of K10(K10( the carrier of T))
a is Element of the carrier of (Closed_Domains_Lattice T)
b is Element of the carrier of (Closed_Domains_Lattice T)
B is Element of Closed_Domains_of T
b is Element of the carrier of (Closed_Domains_Lattice T)
B is Element of Closed_Domains_of T
C is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
c is Element of the carrier of (Closed_Domains_Lattice T)
C 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
Closed_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Closed_Domains_Lattice T) is non empty set
K10( the carrier of (Closed_Domains_Lattice T)) is non empty set
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
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)
X is Element of K10( the carrier of (Closed_Domains_Lattice T))
"/\" (X,(Closed_Domains_Lattice T)) is Element of the carrier of (Closed_Domains_Lattice T)
{ b₁ where b₁ is Element of the carrier of (Closed_Domains_Lattice T) : b₁ is_less_than X } is set
"\/" ( { b₁ where b₁ is Element of the carrier of (Closed_Domains_Lattice T) : b₁ is_less_than X } ,(Closed_Domains_Lattice T)) is Element of the carrier of (Closed_Domains_Lattice T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is closed_condensed } is set
Closed_Domains_of T is non empty Element of K10(K10( the carrier of T))
a is Element of the carrier of (Closed_Domains_Lattice T)
b is Element of the carrier of (Closed_Domains_Lattice T)
B is Element of Closed_Domains_of T
b is Element of the carrier of (Closed_Domains_Lattice T)
B is Element of Closed_Domains_of T
C is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
c is Element of the carrier of (Closed_Domains_Lattice T)
C is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is closed_condensed } is set
Closed_Domains_of T is non empty Element of K10(K10( the carrier of T))
a is Element of the carrier of (Closed_Domains_Lattice T)
b is Element of the carrier of (Closed_Domains_Lattice T)
B is Element of Closed_Domains_of T
b is Element of the carrier of (Closed_Domains_Lattice 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
Domains_Lattice T is non empty Lattice-like V131() complemented LattStr
the carrier of (Domains_Lattice T) is non empty set
K10( the carrier of (Domains_Lattice T)) is non empty set
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
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 (Domains_Lattice T))
"/\" (X,(Domains_Lattice T)) is Element of the carrier of (Domains_Lattice T)
{ b₁ where b₁ is Element of the carrier of (Domains_Lattice T) : b₁ is_less_than X } is set
"\/" ( { b₁ where b₁ is Element of the carrier of (Domains_Lattice T) : b₁ is_less_than X } ,(Domains_Lattice T)) is Element of the carrier of (Domains_Lattice T)
(meet F) /\ (Cl (Int (meet F))) is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
Open_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Open_Domains_Lattice T) is non empty set
Open_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
Open_Domains_Union T is Relation-like Function-like V32(K11((Open_Domains_of T),(Open_Domains_of T)), Open_Domains_of T) Element of K10(K11(K11((Open_Domains_of T),(Open_Domains_of T)),(Open_Domains_of T)))
K11((Open_Domains_of T),(Open_Domains_of T)) is non empty Relation-like set
K11(K11((Open_Domains_of T),(Open_Domains_of T)),(Open_Domains_of T)) is non empty Relation-like set
K10(K11(K11((Open_Domains_of T),(Open_Domains_of T)),(Open_Domains_of T))) is non empty set
Open_Domains_Meet T is Relation-like Function-like V32(K11((Open_Domains_of T),(Open_Domains_of T)), Open_Domains_of T) Element of K10(K11(K11((Open_Domains_of T),(Open_Domains_of T)),(Open_Domains_of T)))
LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #) is strict LattStr
T is non empty TopSpace-like TopStruct
Open_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Open_Domains_Lattice T) is non empty set
the carrier of T is non empty set
K10( the carrier of T) is non empty set
Open_Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
F is Element of the carrier of (Open_Domains_Lattice T)
X is Element of the carrier of (Open_Domains_Lattice T)
F "\/" X is Element of the carrier of (Open_Domains_Lattice T)
F "/\" X is Element of the carrier of (Open_Domains_Lattice T)
A is Element of Open_Domains_of T
a is Element of Open_Domains_of T
A \/ a is Element of K10( the carrier of T)
Cl (A \/ a) is closed Element of K10( the carrier of T)
Int (Cl (A \/ a)) is open Element of K10( the carrier of T)
A /\ a is Element of K10( the carrier of T)
Open_Domains_Union T is Relation-like Function-like V32(K11((Open_Domains_of T),(Open_Domains_of T)), Open_Domains_of T) Element of K10(K11(K11((Open_Domains_of T),(Open_Domains_of T)),(Open_Domains_of T)))
K11((Open_Domains_of T),(Open_Domains_of T)) is non empty Relation-like set
K11(K11((Open_Domains_of T),(Open_Domains_of T)),(Open_Domains_of T)) is non empty Relation-like set
K10(K11(K11((Open_Domains_of T),(Open_Domains_of T)),(Open_Domains_of T))) is non empty set
Open_Domains_Meet T is Relation-like Function-like V32(K11((Open_Domains_of T),(Open_Domains_of T)), Open_Domains_of T) Element of K10(K11(K11((Open_Domains_of T),(Open_Domains_of T)),(Open_Domains_of T)))
LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #) is strict LattStr
(Open_Domains_Union T) . (A,a) is Element of Open_Domains_of T
(Open_Domains_Meet T) . (A,a) is Element of Open_Domains_of T
T is non empty TopSpace-like TopStruct
Open_Domains_Lattice T is non empty Lattice-like Boolean LattStr
Bottom (Open_Domains_Lattice T) is Element of the carrier of (Open_Domains_Lattice T)
the carrier of (Open_Domains_Lattice T) is non empty set
{} 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)
the carrier of T is non empty set
K10( the carrier of T) is non empty set
Top (Open_Domains_Lattice T) is Element of the carrier of (Open_Domains_Lattice T)
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is open_condensed } is set
Open_Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
X is Element of the carrier of (Open_Domains_Lattice T)
A is Element of the carrier of (Open_Domains_Lattice T)
X "\/" A is Element of the carrier of (Open_Domains_Lattice T)
a is Element of Open_Domains_of T
F is Element of Open_Domains_of T
F \/ a is Element of K10( the carrier of T)
Cl (F \/ a) is closed Element of K10( the carrier of T)
Int (Cl (F \/ a)) is open Element of K10( the carrier of T)
b is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is open_condensed } is set
Open_Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
X is Element of the carrier of (Open_Domains_Lattice T)
A is Element of the carrier of (Open_Domains_Lattice T)
X "/\" A is Element of the carrier of (Open_Domains_Lattice T)
F is Element of Open_Domains_of T
a is Element of Open_Domains_of T
F /\ a is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
Open_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Open_Domains_Lattice T) is non empty set
the carrier of T is non empty set
K10( the carrier of T) is non empty set
Open_Domains_of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
F is Element of the carrier of (Open_Domains_Lattice T)
X is Element of the carrier of (Open_Domains_Lattice T)
A is Element of Open_Domains_of T
a is Element of Open_Domains_of T
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is open_condensed } is set
b is Element of K10( the carrier of T)
B is Element of K10( the carrier of T)
F "\/" X is Element of the carrier of (Open_Domains_Lattice T)
A \/ a is Element of K10( the carrier of T)
Cl (A \/ a) is closed Element of K10( the carrier of T)
Int (Cl (A \/ a)) is open Element of K10( the carrier of T)
A \/ a is Element of K10( the carrier of T)
Cl (A \/ a) is closed Element of K10( the carrier of T)
Int (Cl (A \/ a)) is open Element of K10( the carrier of T)
B is Element of K10( the carrier of T)
F "\/" X is Element of the carrier of (Open_Domains_Lattice T)
T is non empty TopSpace-like TopStruct
Open_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Open_Domains_Lattice T) is non empty set
K10( the carrier of (Open_Domains_Lattice T)) is non empty set
F is Element of K10( the carrier of (Open_Domains_Lattice T))
Open_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
X is Element of K10(K10( the carrier of T))
union X is Element of K10( the carrier of T)
Cl (union X) is closed Element of K10( the carrier of T)
Int (Cl (union X)) is open Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is open_condensed } is set
a is Element of the carrier of (Open_Domains_Lattice T)
b is Element of the carrier of (Open_Domains_Lattice T)
B is Element of Open_Domains_of T
C is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
c is Element of the carrier of (Open_Domains_Lattice T)
C is Element of K10( the carrier of T)
b is Element of the carrier of (Open_Domains_Lattice T)
B is Element of Open_Domains_of T
b is Element of the carrier of (Open_Domains_Lattice T)
T is non empty TopSpace-like TopStruct
Open_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Open_Domains_Lattice T) is non empty set
F is set
{ b₁ where b₁ is Element of the carrier of (Open_Domains_Lattice T) : b₁ in F } is set
A is Element of the carrier of (Open_Domains_Lattice T)
a is Element of the carrier of (Open_Domains_Lattice T)
A is Element of the carrier of (Open_Domains_Lattice T)
a is Element of the carrier of (Open_Domains_Lattice T)
b is Element of the carrier of (Open_Domains_Lattice T)
A is set
a is Element of the carrier of (Open_Domains_Lattice T)
K10( the carrier of (Open_Domains_Lattice T)) is non empty set
A is Element of K10( the carrier of (Open_Domains_Lattice T))
a is Element of the carrier of (Open_Domains_Lattice T)
b is Element of the carrier of (Open_Domains_Lattice T)
b is Element of the carrier of (Open_Domains_Lattice 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
Open_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Open_Domains_Lattice T) is non empty set
K10( the carrier of (Open_Domains_Lattice 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)
X is Element of K10( the carrier of (Open_Domains_Lattice T))
"\/" (X,(Open_Domains_Lattice T)) is Element of the carrier of (Open_Domains_Lattice T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is open_condensed } is set
Open_Domains_of T is non empty Element of K10(K10( the carrier of T))
a is Element of the carrier of (Open_Domains_Lattice T)
b is Element of the carrier of (Open_Domains_Lattice T)
B is Element of Open_Domains_of T
b is Element of the carrier of (Open_Domains_Lattice T)
B is Element of Open_Domains_of T
C is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
c is Element of the carrier of (Open_Domains_Lattice T)
C 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
Open_Domains_Lattice T is non empty Lattice-like Boolean LattStr
the carrier of (Open_Domains_Lattice T) is non empty set
K10( the carrier of (Open_Domains_Lattice T)) is non empty set
[#] T is non empty non proper open closed dense non boundary Element of K10( the carrier of T)
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 (Open_Domains_Lattice T))
"/\" (X,(Open_Domains_Lattice T)) is Element of the carrier of (Open_Domains_Lattice T)
{ b₁ where b₁ is Element of the carrier of (Open_Domains_Lattice T) : b₁ is_less_than X } is set
"\/" ( { b₁ where b₁ is Element of the carrier of (Open_Domains_Lattice T) : b₁ is_less_than X } ,(Open_Domains_Lattice T)) is Element of the carrier of (Open_Domains_Lattice T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is open_condensed } is set
Open_Domains_of T is non empty Element of K10(K10( the carrier of T))
a is Element of the carrier of (Open_Domains_Lattice T)
b is Element of the carrier of (Open_Domains_Lattice T)
B is Element of Open_Domains_of T
b is Element of the carrier of (Open_Domains_Lattice T)
B is Element of Open_Domains_of T
C is Element of K10( the carrier of T)
C1 is Element of K10( the carrier of T)
c is Element of the carrier of (Open_Domains_Lattice T)
C is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of K10( the carrier of T) : b₁ is open_condensed } is set
Open_Domains_of T is non empty Element of K10(K10( the carrier of T))
a is Element of the carrier of (Open_Domains_Lattice T)
b is Element of the carrier of (Open_Domains_Lattice T)
B is Element of Open_Domains_of T
b is Element of the carrier of (Open_Domains_Lattice 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
Domains_Lattice T is non empty Lattice-like V131() complemented LattStr
the carrier of (Domains_Lattice T) is non empty set
K10( the carrier of (Domains_Lattice 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)
(union F) \/ (Int (Cl (union F))) is Element of K10( the carrier of T)
X is Element of K10( the carrier of (Domains_Lattice T))
"\/" (X,(Domains_Lattice T)) is Element of the carrier of (Domains_Lattice T)