:: WAYBEL12 semantic presentation

REAL is set

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:]

{ (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
is non empty trivial finite V47() 1 -element countable Element of bool NAT

\/ (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 \/ (Seg I) } is set
S is set

F . p is Element of the carrier of T

S is set

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 \/ (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 \/ (Seg I) } is epsilon-transitive epsilon-connected ordinal cardinal set

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

F is set

T is non trivial non finite countable denumerable 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

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

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

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

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

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

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
{()} 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 "/\" {()} 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 {()} ) } is set
{()} "/\" F is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in {()} & b2 in F ) } is set
{ (() "/\" 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
() "/\" Q is Element of the carrier of T
Q "/\" () is Element of 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
Bottom T is Element of the carrier of 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 "/\" {()} 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 {()} ) } is set
I is set
{ (() "/\" b1) where b1 is Element of the carrier of T : b1 in F } is set
Q is set
S is Element of F
() "/\" S is Element of 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
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

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

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

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
{()} 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 is Element of bool the carrier of T
{ (b1 "\/" b2) where b1, b2 is Element of the carrier of T : ( b1 in {()} & b2 in F ) } is set
{ (() "\/" 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
() "\/" 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
() "\/" 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

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

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

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

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

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

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

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

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

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

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

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
() ` is upper Element of bool the carrier of T
the carrier of T \ () 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

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

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

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

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

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

{ ("/\" (b1,T)) where b1 is finite countable Element of bool F : ex_inf_of b1,T } is set
uparrow () is non empty filtered upper Element of 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
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

{ ("/\" (b1,T)) where b1 is finite countable Element of bool F : ex_inf_of b1,T } is set
uparrow () is non empty filtered upper Element of 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
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

{ ("/\" (b1,T)) where b1 is finite countable Element of bool F : ex_inf_of b1,T } is set
uparrow () is non empty filtered upper Element of bool the carrier of T
I is (T,F)

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

{ ("/\" (b1,T)) where b1 is finite countable Element of bool I : ex_inf_of b1,T } is set
uparrow () is filtered upper Element of 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
F is Element of bool the carrier of T
fininfs F is filtered Element of bool the carrier of T

{ ("/\" (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

{ ("/\" (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,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

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

Y1 is set
p . Y1 is set
Y is 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

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

{ ("/\" (b1,T)) where b1 is finite countable Element of bool I : ex_inf_of b1,T } is set
uparrow () is filtered upper Element of bool the carrier of T
fininfs Q is non empty filtered Element of bool the carrier of T

{ ("/\" (b1,T)) where b1 is finite countable Element of bool Q : ex_inf_of b1,T } is set
uparrow () is non empty filtered upper Element of 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
[: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

p is set
I . p is set

{ (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

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

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

Y is set
S . Y is set

{ (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

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

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

[: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:]

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

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

rng A is Element of bool S

V is non empty Element of bool the carrier of T
fininfs V is non empty filtered Element of bool the carrier of T

{ ("/\" (b1,T)) where b1 is finite countable Element of bool V : ex_inf_of b1,T } is set
uparrow () 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

A . q is Element of S

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

A . x is Element of S

A . (x + 1) is Element of S

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

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

A . q is Element of S

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

x is Element of the carrier of T
x is Element of the carrier of T

"/\" (q,T) is Element of the carrier of T
y is set
A . y is set

A . Y is Element of S

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

A . n is Element of S

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

p . x is Element of the carrier of T

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

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

A . q is Element of S

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,T) is Element of the carrier of T
n is set
A . n is set

A . n is Element of S

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

{ ("/\" (b1,T)) where b1 is finite countable Element of bool P : ex_inf_of b1,T } is set
uparrow () is non empty filtered upper Element of 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
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

{ ("/\" (b1,T)) where b1 is finite countable Element of bool I : ex_inf_of b1,T } is set
uparrow () 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

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

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
() ` is upper Open Element of bool the carrier of T
the carrier of T \ () is set
(() `) "/\" I is Element of bool the carrier of T
{ (b1 "/\" b2) where b1, b2 is Element of the carrier of T : ( b1 in () ` & 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

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

the carrier of T is non empty set
Top T is (T) Element of the carrier of T

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

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

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

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

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

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

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)

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

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
() /\ 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