REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is non empty cup-closed diff-closed preBoolean set
{} is empty V10() non-empty empty-yielding functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() V40() finite finite-yielding V47() cardinal {} -element countable FinSequence-like FinSequence-membered set
the empty V10() non-empty empty-yielding functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() V40() finite finite-yielding V47() cardinal {} -element countable FinSequence-like FinSequence-membered set is empty V10() non-empty empty-yielding functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() V40() finite finite-yielding V47() cardinal {} -element countable FinSequence-like FinSequence-membered set
COMPLEX is set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable set
bool omega is non empty non trivial cup-closed diff-closed preBoolean non finite set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
card omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
0 is empty V10() non-empty empty-yielding functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() V40() finite finite-yielding V47() cardinal {} -element countable FinSequence-like FinSequence-membered Element of NAT
T is non empty RelStr
the carrier of T is non empty set
[:NAT, the carrier of T:] is non empty non trivial V10() non finite set
bool [:NAT, the carrier of T:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]
I is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
{ (F . b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 <= I } is set
{0} is non empty trivial finite V47() 1 -element countable Element of bool NAT
Seg I is finite I -element countable Element of bool NAT
{0} \/ (Seg I) is non empty finite countable Element of bool NAT
{ (F . b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 in {0} \/ (Seg I) } is set
S is set
p is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
F . p is Element of the carrier of T
Seg p is finite p -element countable Element of bool NAT
S is set
p is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
F . p is Element of the carrier of T
{ H1(b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 in {0} \/ (Seg I) } is set
card { H1(b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 in {0} \/ (Seg I) } is epsilon-transitive epsilon-connected ordinal cardinal set
card ({0} \/ (Seg I)) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of omega
F . 0 is Element of the carrier of T
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
F ` is Element of bool the carrier of T
the carrier of T \ F is set
[#] T is non proper dense Element of bool the carrier of T
([#] T) \ F is Element of bool the carrier of T
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
T is set
card T is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
T is non trivial non finite countable denumerable set
card T is non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
card NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set
T is non empty transitive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
I is Element of bool the carrier of T
downarrow F is lower Element of bool the carrier of T
downarrow I is lower Element of bool the carrier of T
Q is set
S is Element of the carrier of T
p is Element of the carrier of T
Y is Element of the carrier of T
T is non empty transitive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
I is Element of bool the carrier of T
F is Element of bool the carrier of T
uparrow F is upper Element of bool the carrier of T
uparrow I is upper Element of bool the carrier of T
Q is set
S is Element of the carrier of T
p is Element of the carrier of T
Y is Element of the carrier of T
T is non empty reflexive transitive antisymmetric RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is non empty finite filtered countable Element of bool the carrier of T
"/\" (F,T) is Element of the carrier of T
I is Element of the carrier of T
T is non empty antisymmetric lower-bounded RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Bottom T is Element of the carrier of T
F is non empty lower Element of bool the carrier of T
I is set
Q is Element of F
T is non empty antisymmetric lower-bounded RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Bottom T is Element of the carrier of T
F is non empty Element of bool the carrier of T
downarrow F is Element of bool the carrier of T
I is set
{ b1 where b1 is Element of the carrier of T : ex b2 being Element of the carrier of T st
( b1 <= b2 & b2 in F ) } is set
Q is Element of F
T is non empty antisymmetric upper-bounded RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Top T is Element of the carrier of T
F is non empty upper Element of bool the carrier of T
I is set
Q is Element of F
T is non empty antisymmetric upper-bounded RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Top T is Element of the carrier of T
F is non empty Element of bool the carrier of T
uparrow F is Element of bool the carrier of T
I is set
{ b1 where b1 is Element of the carrier of T : ex b2 being Element of the carrier of T st
( b2 <= b1 & b2 in F ) } is set
Q is Element of F
T is non empty antisymmetric lower-bounded with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Bottom T is Element of the carrier of T
{(Bottom T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F is Element of bool the carrier of T
F "/\" {(Bottom T)} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {(Bottom T)} ) } is set
{(Bottom T)} "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {(Bottom T)} & b2 in F ) } is set
{ ((Bottom T) "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
I is set
Q is Element of the carrier of T
(Bottom T) "/\" Q is Element of the carrier of T
Q "/\" (Bottom T) is Element of the carrier of T
T is non empty antisymmetric lower-bounded with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Bottom T is Element of the carrier of T
{(Bottom T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F is non empty Element of bool the carrier of T
F "/\" {(Bottom T)} is non empty Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {(Bottom T)} ) } is set
I is set
{ ((Bottom T) "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
Q is set
S is Element of F
(Bottom T) "/\" S is Element of the carrier of T
T is non empty antisymmetric upper-bounded with_suprema RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Top T is Element of the carrier of T
{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F is Element of bool the carrier of T
F "\/" {(Top T)} is Element of bool the carrier of T
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {(Top T)} ) } is set
{(Top T)} "\/" F is Element of bool the carrier of T
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of T : ( b1 in {(Top T)} & b2 in F ) } is set
{ ((Top T) "\/" b1) where b1 is Element of the carrier of T : b1 in F } is set
I is set
Q is Element of the carrier of T
(Top T) "\/" Q is Element of the carrier of T
Q "\/" (Top T) is Element of the carrier of T
T is non empty antisymmetric upper-bounded with_suprema RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Top T is Element of the carrier of T
{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F is non empty Element of bool the carrier of T
F "\/" {(Top T)} is non empty Element of bool the carrier of T
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {(Top T)} ) } is set
I is set
{ ((Top T) "\/" b1) where b1 is Element of the carrier of T : b1 in F } is set
Q is set
S is Element of F
(Top T) "\/" S is Element of the carrier of T
T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Top T is Element of the carrier of T
{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F is Element of bool the carrier of T
{(Top T)} "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {(Top T)} & b2 in F ) } is set
{ ((Top T) "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
I is set
Q is Element of the carrier of T
(Top T) "/\" Q is Element of the carrier of T
I is set
Q is non empty Element of bool the carrier of T
S is Element of Q
(Top T) "/\" S is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Bottom T is Element of the carrier of T
{(Bottom T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F is Element of bool the carrier of T
{(Bottom T)} "\/" F is Element of bool the carrier of T
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of T : ( b1 in {(Bottom T)} & b2 in F ) } is set
{ ((Bottom T) "\/" b1) where b1 is Element of the carrier of T : b1 in F } is set
I is set
Q is Element of the carrier of T
(Bottom T) "\/" Q is Element of the carrier of T
I is set
Q is non empty Element of bool the carrier of T
S is Element of Q
(Bottom T) "\/" S is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
I is Element of bool the carrier of T
Q is Element of the carrier of T
S is Element of the carrier of T
Q is Element of the carrier of T
S is Element of the carrier of T
T is non empty transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
I is Element of the carrier of T
Q is Element of the carrier of T
{I} is non empty trivial finite 1 -element countable Element of bool the carrier of T
{I} "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {I} & b2 in F ) } is set
{Q} is non empty trivial finite 1 -element countable Element of bool the carrier of T
{Q} "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {Q} & b2 in F ) } is set
{ (Q "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
S is Element of the carrier of T
p is Element of the carrier of T
Q "/\" p is Element of the carrier of T
I "/\" p is Element of the carrier of T
Y is Element of the carrier of T
{ (I "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
T is non empty transitive antisymmetric with_suprema RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
I is Element of the carrier of T
Q is Element of the carrier of T
{I} is non empty trivial finite 1 -element countable Element of bool the carrier of T
{I} "\/" F is Element of bool the carrier of T
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of T : ( b1 in {I} & b2 in F ) } is set
{Q} is non empty trivial finite 1 -element countable Element of bool the carrier of T
{Q} "\/" F is Element of bool the carrier of T
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of T : ( b1 in {Q} & b2 in F ) } is set
{ (I "\/" b1) where b1 is Element of the carrier of T : b1 in F } is set
S is Element of the carrier of T
p is Element of the carrier of T
I "\/" p is Element of the carrier of T
Q "\/" p is Element of the carrier of T
Y is Element of the carrier of T
{ (Q "\/" b1) where b1 is Element of the carrier of T : b1 in F } is set
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Q is Element of bool the carrier of T
I is Element of bool the carrier of T
F is Element of bool the carrier of T
S is set
p is non empty Element of bool the carrier of T
Y is Element of p
Y1 is Element of the carrier of T
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
I is Element of bool the carrier of T
Q is Element of bool the carrier of T
F is Element of bool the carrier of T
S is set
p is non empty Element of bool the carrier of T
Y is Element of p
Y1 is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is filtered upper Element of bool the carrier of T
F "/\" F is filtered Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in F ) } is set
I is set
Q is Element of the carrier of T
S is Element of the carrier of T
Q "/\" S is Element of the carrier of T
p is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is directed lower Element of bool the carrier of T
F "\/" F is directed Element of bool the carrier of T
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in F ) } is set
I is set
Q is Element of the carrier of T
S is Element of the carrier of T
Q "\/" S is Element of the carrier of T
p is Element of the carrier of T
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : F "/\" {b1} c= F } is set
Q is set
S is Element of the carrier of T
{S} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {S} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {S} ) } is set
T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : F "/\" {b1} c= F } is set
Top T is Element of the carrier of T
{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {(Top T)} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {(Top T)} ) } is set
T is non empty transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : F "/\" {b1} c= F } is set
I is Element of bool the carrier of T
Q is Element of the carrier of T
S is Element of the carrier of T
p is Element of the carrier of T
{p} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {p} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {p} ) } is set
Y is Element of the carrier of T
{Y} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {Y} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {Y} ) } is set
p "/\" Y is Element of the carrier of T
Y1 is Element of the carrier of T
{Y1} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {Y1} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {Y1} ) } is set
{Y1} "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {Y1} & b2 in F ) } is set
{ (Y1 "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
A is set
q is Element of the carrier of T
Y1 "/\" q is Element of the carrier of T
{p} "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {p} & b2 in F ) } is set
{ (p "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
Y "/\" q is Element of the carrier of T
p "/\" (Y "/\" q) is Element of the carrier of T
{Y} "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {Y} & b2 in F ) } is set
{ (Y "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
T is non empty transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is upper Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : F "/\" {b1} c= F } is set
I is Element of bool the carrier of T
Q is Element of the carrier of T
S is Element of the carrier of T
{S} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {S} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {S} ) } is set
p is Element of the carrier of T
{p} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {p} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {p} ) } is set
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
I is Element of the carrier of T
Q is Element of the carrier of T
I "/\" Q is Element of the carrier of T
S is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
T is non empty reflexive antisymmetric up-complete satisfying_axiom_of_approximation continuous RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
I is Element of the carrier of T
waybelow I is non empty directed Element of bool the carrier of T
Q is set
S is Element of the carrier of T
T is non empty reflexive transitive antisymmetric up-complete with_infima satisfying_axiom_of_approximation continuous RelStr
the carrier of T is non empty set
F is Element of the carrier of T
downarrow F is non empty directed filtered lower Open Element of bool the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
{F} is non empty trivial finite 1 -element countable Element of bool the carrier of T
downarrow {F} is non empty filtered lower Open Element of bool the carrier of T
(downarrow F) ` is upper Element of bool the carrier of T
the carrier of T \ (downarrow F) is set
I is Element of the carrier of T
S is Element of the carrier of T
waybelow S is non empty directed filtered lower Open Element of bool the carrier of T
p is Element of the carrier of T
waybelow p is non empty directed filtered lower Open Element of bool the carrier of T
S is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is non empty Element of bool the carrier of T
bool F is non empty cup-closed diff-closed preBoolean set
Fin F is non empty cup-closed diff-closed preBoolean set
I is non empty finite countable Element of Fin F
"/\" (I,T) is Element of the carrier of T
Q is non empty finite countable Element of Fin F
"/\" (Q,T) is Element of the carrier of T
I \/ Q is non empty finite countable Element of Fin F
"/\" ((I \/ Q),T) is Element of the carrier of T
("/\" (I,T)) "/\" ("/\" (Q,T)) is Element of the carrier of T
I is non empty finite countable Element of bool F
"/\" (I,T) is Element of the carrier of T
Q is Element of F
{Q} is non empty trivial finite 1 -element countable Element of bool F
"/\" ({Q},T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is non empty Element of bool the carrier of T
bool F is non empty cup-closed diff-closed preBoolean set
Fin F is non empty cup-closed diff-closed preBoolean set
I is non empty finite countable Element of Fin F
"\/" (I,T) is Element of the carrier of T
Q is non empty finite countable Element of Fin F
"\/" (Q,T) is Element of the carrier of T
I \/ Q is non empty finite countable Element of Fin F
"\/" ((I \/ Q),T) is Element of the carrier of T
("\/" (I,T)) "\/" ("\/" (Q,T)) is Element of the carrier of T
I is non empty finite countable Element of bool F
"\/" (I,T) is Element of the carrier of T
Q is Element of F
{Q} is non empty trivial finite 1 -element countable Element of bool F
"\/" ({Q},T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is non empty filtered upper Element of bool the carrier of T
fininfs F is non empty filtered Element of bool the carrier of T
bool F is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool F : ex_inf_of b1,T } is set
uparrow (fininfs F) is non empty filtered upper Element of bool the carrier of T
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is non empty filtered upper Element of bool the carrier of T
fininfs F is non empty filtered Element of bool the carrier of T
bool F is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool F : ex_inf_of b1,T } is set
uparrow (fininfs F) is non empty filtered upper Element of bool the carrier of T
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is non empty filtered upper Element of bool the carrier of T
fininfs F is non empty filtered Element of bool the carrier of T
bool F is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool F : ex_inf_of b1,T } is set
uparrow (fininfs F) is non empty filtered upper Element of bool the carrier of T
I is (T,F)
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is non empty filtered upper Element of bool the carrier of T
I is (T,F)
fininfs I is filtered Element of bool the carrier of T
bool I is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool I : ex_inf_of b1,T } is set
uparrow (fininfs I) is filtered upper Element of bool the carrier of T
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of bool the carrier of T
fininfs F is filtered Element of bool the carrier of T
bool F is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool F : ex_inf_of b1,T } is set
I is non empty Element of bool the carrier of T
fininfs I is non empty filtered Element of bool the carrier of T
bool I is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool I : ex_inf_of b1,T } is set
Q is Element of the carrier of T
S is finite countable Element of bool F
"/\" (S,T) is Element of the carrier of T
p is set
Y is Element of the carrier of T
Y1 is Element of the carrier of T
[:S,I:] is V10() set
bool [:S,I:] is non empty cup-closed diff-closed preBoolean set
p is V10() V13(S) V14(I) Function-like V21(S,I) finite countable Element of bool [:S,I:]
p .: S is finite countable Element of bool I
Y is set
dom p is finite countable Element of bool S
bool S is non empty cup-closed diff-closed preBoolean finite V47() countable set
Y1 is set
p . Y1 is set
Y is set
dom p is finite countable Element of bool S
bool S is non empty cup-closed diff-closed preBoolean finite V47() countable set
p . Y is set
"/\" ((p .: S),T) is Element of the carrier of T
Y is Element of the carrier of T
p . Y is set
Y1 is Element of the carrier of T
A is Element of the carrier of T
dom p is finite countable Element of bool S
bool S is non empty cup-closed diff-closed preBoolean finite V47() countable set
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is non empty filtered upper Element of bool the carrier of T
I is (T,F)
Q is non empty Element of bool the carrier of T
fininfs I is filtered Element of bool the carrier of T
bool I is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool I : ex_inf_of b1,T } is set
uparrow (fininfs I) is filtered upper Element of bool the carrier of T
fininfs Q is non empty filtered Element of bool the carrier of T
bool Q is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool Q : ex_inf_of b1,T } is set
uparrow (fininfs Q) is non empty filtered upper Element of bool the carrier of T
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
[:NAT, the carrier of T:] is non empty non trivial V10() non finite set
bool [:NAT, the carrier of T:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
F is Element of bool the carrier of T
I is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]
rng I is Element of bool the carrier of T
Q is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]
rng Q is Element of bool the carrier of T
S is Element of the carrier of T
dom I is countable Element of bool NAT
p is set
I . p is set
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
{ (I . b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 <= Y } is set
Y1 is non empty finite countable Element of bool the carrier of T
"/\" (Y1,T) is Element of the carrier of T
A is Element of the carrier of T
dom Q is countable Element of bool NAT
Q . Y is Element of the carrier of T
I . Y is Element of the carrier of T
{(I . Y)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
"/\" ({(I . Y)},T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
[:NAT, the carrier of T:] is non empty non trivial V10() non finite set
bool [:NAT, the carrier of T:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
F is non empty filtered upper Element of bool the carrier of T
I is (T,F)
Q is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]
rng Q is Element of bool the carrier of T
S is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]
rng S is Element of bool the carrier of T
p is Element of the carrier of T
dom S is countable Element of bool NAT
Y is set
S . Y is set
Y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
{ (Q . b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 <= Y1 } is set
A is non empty finite countable Element of bool the carrier of T
q is set
dom Q is countable Element of bool NAT
p is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
Q . p is Element of the carrier of T
"/\" (A,T) is Element of the carrier of T
S . Y1 is Element of the carrier of T
S . 0 is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is upper Open Element of bool the carrier of T
I is non empty filtered upper Element of bool the carrier of T
F "/\" I is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in I ) } is set
Q is Element of the carrier of T
S is non empty upper Open Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : F "/\" {b1} c= F } is set
Y1 is non empty (T,I)
[:NAT,Y1:] is non empty non trivial V10() non finite set
bool [:NAT,Y1:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
A is V10() V13( NAT ) V14(Y1) Function-like V21( NAT ,Y1) Element of bool [:NAT,Y1:]
rng A is Element of bool Y1
bool Y1 is non empty cup-closed diff-closed preBoolean set
[:NAT, the carrier of T:] is non empty non trivial V10() non finite set
bool [:NAT, the carrier of T:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
q is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]
{ (q . b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 <= a1 } is set
"/\" ( { (q . b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 <= a1 } ,T) is Element of the carrier of T
p is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]
dom p is countable Element of bool NAT
rng p is Element of bool the carrier of T
P is non empty Element of bool the carrier of T
Y is non empty filtered upper Element of bool the carrier of T
A is set
V is Element of the carrier of T
{V} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {V} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {V} ) } is set
{ (V "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
v is set
x is Element of the carrier of T
V "/\" x is Element of the carrier of T
x "/\" V is Element of the carrier of T
A is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
p . (A + 1) is Element of the carrier of T
V is Element of S
v is Element of the carrier of T
{v} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {v} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {v} ) } is set
V "/\" v is Element of the carrier of T
x is Element of the carrier of T
[:NAT,S:] is non empty non trivial V10() non finite set
bool [:NAT,S:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
p is Element of S
A is V10() V13( NAT ) V14(S) Function-like V21( NAT ,S) Element of bool [:NAT,S:]
A . 0 is Element of S
dom A is countable Element of bool NAT
rng A is Element of bool S
bool S is non empty cup-closed diff-closed preBoolean set
V is non empty Element of bool the carrier of T
fininfs V is non empty filtered Element of bool the carrier of T
bool V is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool V : ex_inf_of b1,T } is set
uparrow (fininfs V) is non empty filtered upper Element of bool the carrier of T
x is Element of the carrier of T
x is Element of the carrier of T
q is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . q is Element of S
q + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . (q + 1) is Element of S
p . (q + 1) is Element of the carrier of T
y is Element of S
Y is Element of S
n is Element of the carrier of T
y "/\" n is Element of the carrier of T
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . x is Element of S
x + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . (x + 1) is Element of S
q is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . q is Element of S
Y is Element of the carrier of T
y is Element of the carrier of T
x is Element of the carrier of T
q is Element of the carrier of T
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . x is Element of S
x is Element of the carrier of T
x is Element of the carrier of T
x is Element of the carrier of T
q is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . q is Element of S
y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . y is Element of S
x is Element of the carrier of T
x is Element of the carrier of T
q is set
A . q is set
Y is set
A . Y is set
y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
x is Element of the carrier of T
x is Element of the carrier of T
q is finite countable Element of bool V
"/\" (q,T) is Element of the carrier of T
y is set
A . y is set
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . Y is Element of S
Y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . (Y + 1) is Element of S
p . (Y + 1) is Element of the carrier of T
n is Element of S
n is Element of S
x1 is Element of the carrier of T
n "/\" x1 is Element of the carrier of T
y is set
Y is Element of the carrier of T
n is set
A . n is set
Top T is Element of the carrier of T
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . n is Element of S
n + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . (n + 1) is Element of S
p . (n + 1) is Element of the carrier of T
x1 is Element of S
y1 is Element of S
z1 is Element of the carrier of T
x1 "/\" z1 is Element of the carrier of T
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
p . x is Element of the carrier of T
x + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
p . (x + 1) is Element of the carrier of T
x is Element of the carrier of T
q is Element of the carrier of T
{ (q . b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 <= x } is set
{ (q . b1) where b1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT : b1 <= x + 1 } is set
y is non empty finite countable Element of bool the carrier of T
Y is non empty finite countable Element of bool the carrier of T
n is set
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
q . n is Element of the carrier of T
"/\" (y,T) is Element of the carrier of T
"/\" (Y,T) is Element of the carrier of T
x is Element of the carrier of T
x is set
p . x is set
q is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . q is Element of S
q + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . (q + 1) is Element of S
p . (q + 1) is Element of the carrier of T
y is Element of S
Y is Element of S
n is Element of the carrier of T
y "/\" n is Element of the carrier of T
x is non empty filtered upper Open Element of bool the carrier of T
x is set
q is Element of x
y is Element of the carrier of T
Y is finite countable Element of bool V
"/\" (Y,T) is Element of the carrier of T
n is set
A . n is set
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . n is Element of S
n + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT
A . (n + 1) is Element of S
p . (n + 1) is Element of the carrier of T
x1 is Element of S
y1 is Element of S
z1 is Element of the carrier of T
x1 "/\" z1 is Element of the carrier of T
Top T is Element of the carrier of T
fininfs P is non empty filtered Element of bool the carrier of T
bool P is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool P : ex_inf_of b1,T } is set
uparrow (fininfs P) is non empty filtered upper Element of bool the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is upper Open Element of bool the carrier of T
I is non empty countable Element of bool the carrier of T
F "/\" I is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in I ) } is set
Q is Element of the carrier of T
{Q} is non empty trivial finite 1 -element countable Element of bool the carrier of T
{Q} "/\" I is non empty Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {Q} & b2 in I ) } is set
{ b1 where b1 is Element of the carrier of T : F "/\" {b1} c= F } is set
S is non empty filtered upper Element of bool the carrier of T
p is set
Y is Element of the carrier of T
{Y} is non empty trivial finite 1 -element countable Element of bool the carrier of T
{Y} "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {Y} & b2 in F ) } is set
{ (Y "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
F "/\" {Y} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {Y} ) } is set
Y1 is set
A is Element of the carrier of T
Y "/\" A is Element of the carrier of T
I "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in I & b2 in F ) } is set
fininfs I is non empty filtered Element of bool the carrier of T
bool I is non empty cup-closed diff-closed preBoolean set
{ ("/\" (b1,T)) where b1 is finite countable Element of bool I : ex_inf_of b1,T } is set
uparrow (fininfs I) is non empty filtered upper Element of bool the carrier of T
p is non empty filtered upper Element of bool the carrier of T
F "/\" p is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in p ) } is set
Y is set
Y1 is Element of the carrier of T
A is Element of the carrier of T
Y1 "/\" A is Element of the carrier of T
q is Element of the carrier of T
{q} is non empty trivial finite 1 -element countable Element of bool the carrier of T
F "/\" {q} is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in {q} ) } is set
Y is non empty filtered upper Open Element of bool the carrier of T
{ (Q "/\" b1) where b1 is Element of the carrier of T : b1 in I } is set
Y1 is set
A is Element of the carrier of T
Q "/\" A is Element of the carrier of T
Y "/\" Y is non empty filtered Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in Y & b2 in Y ) } is set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is upper Open Element of bool the carrier of T
I is non empty countable Element of bool the carrier of T
F "/\" I is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in F & b2 in I ) } is set
S is Element of the carrier of T
Q is Element of the carrier of T
{S} is non empty trivial finite 1 -element countable Element of bool the carrier of T
{S} "/\" I is non empty Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {S} & b2 in I ) } is set
uparrow ({S} "/\" I) is non empty upper Element of bool the carrier of T
p is non empty filtered upper Open Element of bool the carrier of T
uparrow p is non empty filtered upper Element of bool the carrier of T
p ` is filtered lower Open Element of bool the carrier of T
the carrier of T \ p is set
Y is Element of the carrier of T
Y1 is meet-irreducible Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of the carrier of T
I is non empty countable Element of bool the carrier of T
downarrow F is non empty directed filtered lower Open Element of bool the carrier of T
{F} is non empty trivial finite 1 -element countable Element of bool the carrier of T
downarrow {F} is non empty filtered lower Open Element of bool the carrier of T
(downarrow F) ` is upper Open Element of bool the carrier of T
the carrier of T \ (downarrow F) is set
((downarrow F) `) "/\" I is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in (downarrow F) ` & b2 in I ) } is set
S is set
p is Element of the carrier of T
Y is Element of the carrier of T
p "/\" Y is Element of the carrier of T
S is Element of the carrier of T
{S} is non empty trivial finite 1 -element countable Element of bool the carrier of T
{S} "/\" I is non empty Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {S} & b2 in I ) } is set
uparrow ({S} "/\" I) is non empty upper Element of bool the carrier of T
T is non empty RelStr
the carrier of T is non empty set
T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
Top T is Element of the carrier of T
the carrier of T is non empty set
F is Element of the carrier of T
Bottom T is Element of the carrier of T
(Top T) "/\" F is Element of the carrier of T
(Top T) "/\" F is Element of the carrier of T
T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of T is non empty set
Top T is (T) Element of the carrier of T
T is non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_infima RelStr
the carrier of T is non empty non trivial set
Bottom T is Element of the carrier of T
F is Element of the carrier of T
Top T is (T) Element of the carrier of T
F "/\" (Top T) is Element of the carrier of T
T is non empty RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of T is non empty set
Top T is (T) Element of the carrier of T
{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
F is Element of the carrier of T
T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Top T is (T) Element of the carrier of T
{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
Bottom T is Element of the carrier of T
Top T is (T) Element of the carrier of T
F is non empty countable (T) Element of bool the carrier of T
I is Element of the carrier of T
{I} is non empty trivial finite 1 -element countable Element of bool the carrier of T
{I} "/\" F is non empty Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {I} & b2 in F ) } is set
uparrow ({I} "/\" F) is non empty upper Element of bool the carrier of T
S is Element of the carrier of T
Q is Element of the carrier of T
S "/\" Q is Element of the carrier of T
Q is meet-irreducible Element of the carrier of T
T is non empty TopSpace-like TopStruct
the topology of T is non empty Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
F is Element of the carrier of (InclPoset the topology of T)
I is Element of bool the carrier of T
I ` is Element of bool the carrier of T
the carrier of T \ I is set
Q is Element of the carrier of (InclPoset the topology of T)
S is Element of the carrier of (InclPoset the topology of T)
Q "/\" S is Element of the carrier of (InclPoset the topology of T)
Q "/\" S is Element of the carrier of (InclPoset the topology of T)
Y is Element of bool the carrier of T
Y ` is Element of bool the carrier of T
the carrier of T \ Y is set
p is Element of bool the carrier of T
p /\ Y is Element of bool the carrier of T
Q /\ S is set
p ` is Element of bool the carrier of T
the carrier of T \ p is set
(p `) \/ (Y `) is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the topology of T is non empty Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
Top (InclPoset the topology of T) is ( InclPoset the topology of T) Element of the carrier of (InclPoset the topology of T)
F is Element of the carrier of (InclPoset the topology of T)
I is Element of bool the carrier of T
I ` is Element of bool the carrier of T
the carrier of T \ I is set
the carrier of T \ I is Element of bool the carrier of T
(I `) ` is Element of bool the carrier of T
the carrier of T \ (I `) is set
Q is Element of bool the carrier of T
S is Element of bool the carrier of T
Q \/ S is Element of bool the carrier of T
Q ` is Element of bool the carrier of T
the carrier of T \ Q is set
S ` is Element of bool the carrier of T
the carrier of T \ S is set
(Q `) /\ (S `) is Element of bool the carrier of T
p is Element of the carrier of (InclPoset the topology of T)
Y is Element of the carrier of (InclPoset the topology of T)
p /\ Y is set
(Q \/ S) ` is Element of bool the carrier of T
the carrier of T \ (Q \/ S) is set
p "/\" Y is Element of the carrier of (InclPoset the topology of T)
T is non empty TopSpace-like TopStruct
the topology of T is non empty Element of bool (bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() RelStr
the carrier of (InclPoset the topology of T) is non empty non trivial set
F is Element of the carrier of (InclPoset the topology of T)
I is Element of bool the carrier of T
Bottom (InclPoset the topology of T) is Element of the carrier of (InclPoset the topology of T)
Q is Element of bool the carrier of T
I /\ Q is Element of bool the carrier of T
S is Element of the carrier of (InclPoset the topology of T)
F /\ S is set
F "/\" S is Element of the carrier of (InclPoset the topology of T)
Q is Element of the carrier of (InclPoset the topology of T)
F "/\" Q is Element of the carrier of (InclPoset the topology of T)
S is Element of bool the carrier of T
I /\ S is Element of bool the carrier of T
F "/\" Q is Element of the carrier of (InclPoset the topology of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
the topology of T is non empty Element of bool (bool the carrier of T)
InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() RelStr
F is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr
the carrier of F is non empty set
I is countable Element of bool (bool the carrier of T)
Q is set
S is Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of F : ex b2 being Element of bool the carrier of T st
( b2 in I & b2 = b1 & b1 is (F) ) } is set
Y1 is set
A is Element of the carrier of F
q is Element of bool the carrier of T
bool the carrier of F is non empty cup-closed diff-closed preBoolean set
Y1 is Element of bool the carrier of F
A is set
q is Element of the carrier of F
p is Element of bool the carrier of T
A is Element of the carrier of F
q is Element of the carrier of F
p is Element of bool the carrier of T
A is non empty Element of bool the carrier of T
p is Element of the carrier of F
q is Element of the carrier of F
Bottom F is Element of the carrier of F
Top F is (F) Element of the carrier of F
{q} is non empty trivial finite 1 -element countable Element of bool the carrier of F
{q} "/\" Y1 is Element of bool the carrier of F
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of F : ( b1 in {q} & b2 in Y1 ) } is set
uparrow ({q} "/\" Y1) is upper Element of bool the carrier of F
p is meet-irreducible Element of the carrier of F
P is Element of bool the carrier of T
P ` is Element of bool the carrier of T
the carrier of T \ P is set
A is non empty irreducible Element of bool the carrier of T
A /\ A is Element of bool the carrier of T
V is Element of bool the carrier of T
x is Element of the carrier of F
q "/\" x is Element of the carrier of F
v is Element of the carrier of F
q "/\" v is Element of the carrier of F
A /\ V is Element of bool the carrier of T
q /\ v is set
A ` is Element of bool the carrier of T
the carrier of T \ A is set
x is set
x is Element of the carrier of T
(A /\ V) /\ A is Element of bool the carrier of T
(A /\ A) /\ V is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
bool the carrier of T is non empty cup-closed diff-closed preBoolean Element of bool (bool the carrier of T)
I is Element of bool (bool the carrier of T)
Intersect I is Element of bool the carrier of T
Q is Element of bool the carrier of T
I is Element of bool (bool the carrier of T)
Intersect I is Element of bool the carrier of T
{ (Int b1) where b1 is Element of bool the carrier of T : b1 in I } is set
[:(bool the carrier of T),(bool the carrier of T):] is non empty V10() set
bool [:(bool the carrier of T),(bool the carrier of T):] is non empty cup-closed diff-closed preBoolean set
S is V10() V13( bool the carrier of T) V14( bool the carrier of T) Function-like V21( bool the carrier of T, bool the carrier of T) Element of bool [:(bool the carrier of T),(bool the carrier of T):]
S .: I is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
p is set
Y is Element of bool the carrier of T
Int Y is open Element of bool the carrier of T
dom S is Element of bool (bool the carrier of T)
S . Y is Element of bool the carrier of T
card { (Int b1) where b1 is Element of bool the carrier of T : b1 in I } is epsilon-transitive epsilon-connected ordinal cardinal set
card I is epsilon-transitive epsilon-connected ordinal cardinal set
Y is set
Y1 is Element of bool the carrier of T
Int Y1 is open Element of bool the carrier of T
p is Element of bool the carrier of T
Y is Element of bool (bool the carrier of T)
Intersect Y is Element of bool the carrier of T
Y1 is set
A is Element of bool the carrier of T
Int A is open Element of bool the carrier of T
q is set
Y1 is Element of bool the carrier of T
A is Element of bool the carrier of T
Int A is open Element of bool the carrier of T
Y1 is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty cup-closed diff-closed preBoolean set
bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set
F is Element of bool (bool the carrier of T)
Intersect F is Element of bool the carrier of T
I is Element of bool the carrier of T
I is Element of bool the carrier of T
I is Element of bool the carrier of T
Q is Element of bool the carrier of T
S is non empty irreducible Element of bool the carrier of T
S /\ Q is Element of bool the carrier of T
p is Element of the carrier of T
{p} is non empty trivial finite 1 -element countable Element of bool the carrier of T
Cl {p} is closed Element of bool the carrier of T
Y is set
Y1 is Element of bool the carrier of T
(S /\ Q) /\ Y1 is Element of bool the carrier of T
Q /\ Y1 is Element of bool the carrier of T
(Q /\ Y1) ` is Element of bool the carrier of T
the carrier of T \ (Q /\ Y1) is set
Cl ((Q /\ Y1) `) is closed Element of bool the carrier of T
S /\ (Q /\ Y1) is Element of bool the carrier of T
Y is set
Y is set
(Intersect F) /\ Q is Element of bool the carrier of T
[#] T is non empty non proper open closed dense non boundary Element of bool the carrier of T