:: WAYBEL21 semantic presentation

K146() is Element of K22(K142())
K142() is set
K22(K142()) is non empty set
K94() is set
K22(K94()) is non empty set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V43() set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V43() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty finite finite-yielding V43() set
1 is non empty set
{{},1} is non empty finite set
K22(K146()) is non empty set
K290() is TopStruct
the carrier of K290() is set
T is non empty reflexive transitive antisymmetric with_infima RelStr
S is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
K22( the carrier of T) is non empty set
Top S is Element of the carrier of S
"/\" ({},S) is Element of the carrier of S
the carrier of T --> (Top S) is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) Element of K22(K23( the carrier of T, the carrier of S))
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) Element of K22(K23( the carrier of T, the carrier of S))
Y is finite Element of K22( the carrier of T)
X .: Y is finite Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
"/\" ((X .: Y),S) is Element of the carrier of S
"/\" (Y,T) is Element of the carrier of T
X . ("/\" (Y,T)) is Element of the carrier of S
X . ("/\" (Y,T)) is Element of the carrier of S
F is non empty Element of K22( the carrier of T)
the Element of F is Element of F
dom X is Element of K22( the carrier of T)
jN is Element of the carrier of T
X . jN is Element of the carrier of S
{(Top S)} is non empty finite Element of K22( the carrier of S)
X . ("/\" (Y,T)) is Element of the carrier of S
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) Element of K22(K23( the carrier of T, the carrier of S))
Y is Element of the carrier of T
F is Element of the carrier of T
X . Y is Element of the carrier of S
X . F is Element of the carrier of S
Y "/\" F is Element of the carrier of T
X . Y is Element of the carrier of S
X . F is Element of the carrier of S
(X . Y) "/\" (X . F) is Element of the carrier of S
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of S is non empty set
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) (T,S)
Y is Element of the carrier of T
F is Element of the carrier of T
{Y,F} is non empty finite Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of S is non empty set
Top T is Element of the carrier of T
"/\" ({},T) is Element of the carrier of T
Top S is Element of the carrier of S
"/\" ({},S) is Element of the carrier of S
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone meet-preserving (T,S)
X . (Top T) is Element of the carrier of S
{} T is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper finite finite-yielding V43() directed filtered Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
"/\" (({} T),T) is Element of the carrier of T
X . ("/\" (({} T),T)) is Element of the carrier of S
X .: ({} T) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper finite finite-yielding V43() directed filtered Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
"/\" ((X .: ({} T)),S) is Element of the carrier of S
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
K22( the carrier of T) is non empty set
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) Element of K22(K23( the carrier of T, the carrier of S))
Y is non empty finite Element of K22( the carrier of T)
X .: Y is non empty finite Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
"/\" ((X .: Y),S) is Element of the carrier of S
"/\" (Y,T) is Element of the carrier of T
X . ("/\" (Y,T)) is Element of the carrier of S
X .: {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper finite finite-yielding V43() directed filtered Element of K22( the carrier of S)
"/\" ((X .: {}),S) is Element of the carrier of S
"/\" ({},T) is Element of the carrier of T
X . ("/\" ({},T)) is Element of the carrier of S
F is set
iN is set
X .: iN is Element of K22( the carrier of S)
"/\" ((X .: iN),S) is Element of the carrier of S
"/\" (iN,T) is Element of the carrier of T
X . ("/\" (iN,T)) is Element of the carrier of S
{F} is non empty finite set
iN \/ {F} is non empty set
X .: (iN \/ {F}) is Element of K22( the carrier of S)
"/\" ((X .: (iN \/ {F})),S) is Element of the carrier of S
"/\" ((iN \/ {F}),T) is Element of the carrier of T
X . ("/\" ((iN \/ {F}),T)) is Element of the carrier of S
jN is Element of the carrier of T
X . jN is Element of the carrier of S
{(X . jN)} is non empty finite Element of K22( the carrier of S)
"/\" ({(X . jN)},S) is Element of the carrier of S
{jN} is non empty finite Element of K22( the carrier of T)
"/\" ({jN},T) is Element of the carrier of T
dom X is Element of K22( the carrier of T)
Im (X,F) is set
X .: {F} is finite set
(X .: iN) \/ {(X . jN)} is non empty Element of K22( the carrier of S)
(X . ("/\" (iN,T))) "/\" (X . jN) is Element of the carrier of S
("/\" (iN,T)) "/\" jN is Element of the carrier of T
X . (("/\" (iN,T)) "/\" jN) is Element of the carrier of S
X . ("/\" (Y,T)) is Element of the carrier of S
T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
Top T is Element of the carrier of T
"/\" ({},T) is Element of the carrier of T
Top S is Element of the carrier of S
"/\" ({},S) is Element of the carrier of S
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone meet-preserving Element of K22(K23( the carrier of T, the carrier of S))
X . (Top T) is Element of the carrier of S
K22( the carrier of T) is non empty set
Y is finite Element of K22( the carrier of T)
X .: {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper finite finite-yielding V43() directed filtered Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
K22( the carrier of T) is non empty set
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) Element of K22(K23( the carrier of T, the carrier of S))
Y is non empty Element of K22( the carrier of T)
X .: Y is non empty Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
"/\" ((X .: Y),S) is Element of the carrier of S
"/\" (Y,T) is Element of the carrier of T
X . ("/\" (Y,T)) is Element of the carrier of S
K22(Y) is non empty set
F is set
the Element of Y is Element of Y
{ the Element of Y} is non empty finite Element of K22(Y)
jN is Element of the carrier of T
{jN} is non empty finite Element of K22( the carrier of T)
"/\" ({jN},T) is Element of the carrier of T
j is set
Xj is finite Element of K22(Y)
Xj is finite Element of K22(Y)
j is Element of K22( the carrier of T)
"/\" (Xj,T) is Element of the carrier of T
j is non empty Element of K22( the carrier of T)
Xj is Element of the carrier of T
j is non empty finite Element of K22(Y)
"/\" (j,T) is Element of the carrier of T
X .: j is non empty Element of K22( the carrier of S)
"/\" ((X .: j),S) is Element of the carrier of S
"/\" (j,T) is Element of the carrier of T
X . ("/\" (j,T)) is Element of the carrier of S
Xj is set
{Xj} is non empty finite set
j is finite Element of K22(Y)
G is Element of the carrier of T
"/\" (j,T) is Element of the carrier of T
X . ("/\" (Y,T)) is Element of the carrier of S
Xj is Element of the carrier of S
Xj is Element of the carrier of S
j is Element of the carrier of S
dom X is Element of K22( the carrier of T)
G is set
X . G is set
C is non empty finite Element of K22(Y)
"/\" (C,T) is Element of the carrier of T
z is Element of K22( the carrier of T)
X .: z is Element of K22( the carrier of S)
"/\" ((X .: z),S) is Element of the carrier of S
T is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric with_infima RelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) Element of K22(K23( the carrier of T, the carrier of S))
K22( the carrier of T) is non empty set
Y is Element of K22( the carrier of T)
X .: Y is Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
F is finite Element of K22( the carrier of T)
T is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
X is non empty RelStr
the carrier of X is non empty set
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K22(K23( the carrier of X, the carrier of X))
K23( the carrier of X, the carrier of X) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of X)) is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr
S is non empty RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
Y is non empty RelStr
the carrier of Y is non empty set
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
K23( the carrier of X, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of Y)) is non empty set
F is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) Element of K22(K23( the carrier of T, the carrier of S))
iN is Relation-like the carrier of X -defined the carrier of Y -valued Function-like V29( the carrier of X, the carrier of Y) Element of K22(K23( the carrier of X, the carrier of Y))
K22( the carrier of T) is non empty set
K22( the carrier of X) is non empty set
jN is Element of K22( the carrier of X)
K22( the carrier of T) is non empty set
K22( the carrier of X) is non empty set
jN is Element of K22( the carrier of X)
j is Element of K22( the carrier of T)
T is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
X is non empty RelStr
the carrier of X is non empty set
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K22(K23( the carrier of X, the carrier of X))
K23( the carrier of X, the carrier of X) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of X)) is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr
S is non empty RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
Y is non empty RelStr
the carrier of Y is non empty set
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
K23( the carrier of X, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of Y)) is non empty set
F is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) Element of K22(K23( the carrier of T, the carrier of S))
iN is Relation-like the carrier of X -defined the carrier of Y -valued Function-like V29( the carrier of X, the carrier of Y) Element of K22(K23( the carrier of X, the carrier of Y))
K22( the carrier of T) is non empty set
K22( the carrier of X) is non empty set
jN is Element of K22( the carrier of X)
K22( the carrier of T) is non empty set
K22( the carrier of X) is non empty set
jN is Element of K22( the carrier of X)
j is Element of K22( the carrier of T)
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting with_infima SubRelStr of T
incl (S,T) is Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S, the carrier of T) monotone Element of K22(K23( the carrier of S, the carrier of T))
the carrier of S is non empty set
the carrier of T is non empty set
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
K22( the carrier of S) is non empty set
Y is Element of K22( the carrier of S)
(incl (S,T)) .: Y is Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
"/\" (((incl (S,T)) .: Y),T) is Element of the carrier of T
"/\" (Y,S) is Element of the carrier of S
(incl (S,T)) . ("/\" (Y,S)) is Element of the carrier of T
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
(incl (S,T)) . ("/\" (Y,S)) is Element of the carrier of T
"/\" (Y,T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty reflexive transitive antisymmetric full join-inheriting sups-inheriting directed-sups-inheriting with_suprema SubRelStr of T
incl (S,T) is Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S, the carrier of T) monotone Element of K22(K23( the carrier of S, the carrier of T))
the carrier of S is non empty set
the carrier of T is non empty set
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
K22( the carrier of S) is non empty set
Y is Element of K22( the carrier of S)
(incl (S,T)) .: Y is Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
"\/" (((incl (S,T)) .: Y),T) is Element of the carrier of T
"\/" (Y,S) is Element of the carrier of S
(incl (S,T)) . ("\/" (Y,S)) is Element of the carrier of T
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
(incl (S,T)) . ("\/" (Y,S)) is Element of the carrier of T
"\/" (Y,T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric up-complete RelStr
S is non empty reflexive transitive antisymmetric full directed-sups-inheriting SubRelStr of T
incl (S,T) is Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S, the carrier of T) monotone Element of K22(K23( the carrier of S, the carrier of T))
the carrier of S is non empty set
the carrier of T is non empty set
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
K22( the carrier of S) is non empty set
Y is Element of K22( the carrier of S)
(incl (S,T)) .: Y is Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
"\/" (((incl (S,T)) .: Y),T) is Element of the carrier of T
"\/" (Y,S) is Element of the carrier of S
(incl (S,T)) . ("\/" (Y,S)) is Element of the carrier of T
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
F is non empty directed Element of K22( the carrier of T)
(incl (S,T)) . ("\/" (Y,S)) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty reflexive transitive antisymmetric full filtered-infs-inheriting SubRelStr of T
incl (S,T) is Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S, the carrier of T) monotone Element of K22(K23( the carrier of S, the carrier of T))
the carrier of S is non empty set
the carrier of T is non empty set
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
K22( the carrier of S) is non empty set
Y is Element of K22( the carrier of S)
(incl (S,T)) .: Y is Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
"/\" (((incl (S,T)) .: Y),T) is Element of the carrier of T
"/\" (Y,S) is Element of the carrier of S
(incl (S,T)) . ("/\" (Y,S)) is Element of the carrier of T
id the carrier of S is Relation-like the carrier of S -defined the carrier of S -valued Function-like one-to-one non empty V24( the carrier of S) Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
(incl (S,T)) . ("/\" (Y,S)) is Element of the carrier of T
T is RelStr
the carrier of T is set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
S is RelStr
the carrier of S is set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like set
K22(K23( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
X is RelStr
the carrier of X is set
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K22(K23( the carrier of X, the carrier of X))
K23( the carrier of X, the carrier of X) is Relation-like set
K22(K23( the carrier of X, the carrier of X)) is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr
Y is SubRelStr of T
the carrier of Y is set
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr
the InternalRel of T |_2 the carrier of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of K22(K23( the carrier of Y, the carrier of Y))
the InternalRel of T /\ K23( the carrier of Y, the carrier of Y) is Relation-like the carrier of T -defined the carrier of T -valued set
T is non empty RelStr
S is full SubRelStr of T
the carrier of S is set
K22( the carrier of S) is non empty set
X is Element of K22( the carrier of S)
"/\" (X,T) is Element of the carrier of T
the carrier of T is non empty set
the carrier of S is set
K22( the carrier of S) is non empty set
X is Element of K22( the carrier of S)
"\/" (X,T) is Element of the carrier of T
the carrier of T is non empty set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
T is non empty reflexive transitive antisymmetric with_infima RelStr
S is non empty reflexive transitive antisymmetric full SubRelStr of T
the carrier of S is non empty set
K22( the carrier of S) is non empty set
X is non empty finite Element of K22( the carrier of S)
"/\" ({},T) is Element of the carrier of T
the carrier of T is non empty set
Y is set
F is set
"/\" (F,T) is Element of the carrier of T
{Y} is non empty finite set
F \/ {Y} is non empty set
"/\" ((F \/ {Y}),T) is Element of the carrier of T
iN is Element of the carrier of S
K22( the carrier of T) is non empty set
jN is Element of the carrier of T
{jN} is non empty finite Element of K22( the carrier of T)
"/\" ({jN},T) is Element of the carrier of T
j is finite Element of K22( the carrier of T)
j \/ {jN} is non empty finite Element of K22( the carrier of T)
"/\" ((j \/ {jN}),T) is Element of the carrier of T
"/\" (j,T) is Element of the carrier of T
("/\" (j,T)) "/\" jN is Element of the carrier of T
{("/\" (j,T)),jN} is non empty finite Element of K22( the carrier of T)
"/\" ({("/\" (j,T)),jN},T) is Element of the carrier of T
"/\" (X,T) is Element of the carrier of T
X is Element of the carrier of T
Y is Element of the carrier of T
{X,Y} is non empty finite Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
"/\" ({X,Y},T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric with_suprema RelStr
S is non empty reflexive transitive antisymmetric full SubRelStr of T
the carrier of S is non empty set
K22( the carrier of S) is non empty set
X is non empty finite Element of K22( the carrier of S)
"\/" ({},T) is Element of the carrier of T
the carrier of T is non empty set
Y is set
F is set
"\/" (F,T) is Element of the carrier of T
iN is Element of the carrier of S
{Y} is non empty finite set
F \/ {Y} is non empty set
"\/" ((F \/ {Y}),T) is Element of the carrier of T
K22( the carrier of T) is non empty set
jN is Element of the carrier of T
{jN} is non empty finite Element of K22( the carrier of T)
"\/" ({jN},T) is Element of the carrier of T
j is finite Element of K22( the carrier of T)
j \/ {jN} is non empty finite Element of K22( the carrier of T)
"\/" ((j \/ {jN}),T) is Element of the carrier of T
"\/" (j,T) is Element of the carrier of T
("\/" (j,T)) "\/" jN is Element of the carrier of T
{("\/" (j,T)),jN} is non empty finite Element of K22( the carrier of T)
"\/" ({("\/" (j,T)),jN},T) is Element of the carrier of T
"\/" (X,T) is Element of the carrier of T
X is Element of the carrier of T
Y is Element of the carrier of T
{X,Y} is non empty finite Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
"\/" ({X,Y},T) is Element of the carrier of T
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
"/\" ({},T) is Element of the carrier of T
S is non empty reflexive transitive antisymmetric full meet-inheriting with_infima SubRelStr of T
the carrier of S is non empty set
K22( the carrier of S) is non empty set
X is Element of K22( the carrier of S)
"/\" (X,T) is Element of the carrier of T
K22( the carrier of T) is non empty set
Y is Element of K22( the carrier of T)
fininfs Y is non empty filtered Element of K22( the carrier of T)
K22(Y) is non empty set
{ ("/\" (b₁,T)) where b₁ is finite Element of K22(Y) : ex_inf_of b₁,T } is set
"/\" ((fininfs Y),T) is Element of the carrier of T
"/\" (Y,T) is Element of the carrier of T
iN is set
jN is finite Element of K22(Y)
"/\" (jN,T) is Element of the carrier of T
j is finite Element of K22( the carrier of T)
Xj is finite Element of K22( the carrier of S)
iN is non empty Element of K22( the carrier of S)
j is finite Element of K22(Y)
j is Element of the carrier of T
Xj is finite Element of K22(Y)
"/\" (Xj,T) is Element of the carrier of T
j is finite Element of K22(Y)
Xj is finite Element of K22( the carrier of T)
"/\" (j,T) is Element of the carrier of T
jN is non empty filtered Element of K22( the carrier of S)
T is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr
Bottom T is Element of the carrier of T
the carrier of T is non empty set
"\/" ({},T) is Element of the carrier of T
S is non empty reflexive transitive antisymmetric full join-inheriting with_suprema SubRelStr of T
the carrier of S is non empty set
K22( the carrier of S) is non empty set
X is Element of K22( the carrier of S)
"\/" (X,T) is Element of the carrier of T
K22( the carrier of T) is non empty set
Y is Element of K22( the carrier of T)
finsups Y is non empty directed Element of K22( the carrier of T)
K22(Y) is non empty set
{ ("\/" (b₁,T)) where b₁ is finite Element of K22(Y) : ex_sup_of b₁,T } is set
"\/" ((finsups Y),T) is Element of the carrier of T
"\/" (Y,T) is Element of the carrier of T
iN is set
jN is finite Element of K22(Y)
"\/" (jN,T) is Element of the carrier of T
j is finite Element of K22( the carrier of T)
Xj is finite Element of K22( the carrier of S)
iN is non empty Element of K22( the carrier of S)
j is finite Element of K22(Y)
j is Element of the carrier of T
Xj is finite Element of K22(Y)
"\/" (Xj,T) is Element of the carrier of T
j is finite Element of K22(Y)
Xj is finite Element of K22( the carrier of T)
"\/" (j,T) is Element of the carrier of T
jN is non empty directed Element of K22( the carrier of S)
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty reflexive transitive antisymmetric full SubRelStr of T
X is set
the carrier of S is non empty set
X /\ the carrier of S is set
K22( the carrier of S) is non empty set
F is Element of K22( the carrier of S)
"/\" (F,T) is Element of the carrier of T
the carrier of T is non empty set
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty reflexive transitive antisymmetric full SubRelStr of T
X is set
the carrier of S is non empty set
X /\ the carrier of S is set
K22( the carrier of S) is non empty set
F is Element of K22( the carrier of S)
"\/" (F,T) is Element of the carrier of T
the carrier of T is non empty set
T is non empty RelStr
S is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
X is non empty full SubRelStr of T
the carrier of X is non empty set
Y is non empty full SubRelStr of S
the carrier of Y is non empty set
K22( the carrier of X) is non empty set
K22( the carrier of Y) is non empty set
F is Element of K22( the carrier of Y)
"/\" (F,S) is Element of the carrier of S
iN is Element of K22( the carrier of X)
"/\" (iN,T) is Element of the carrier of T
T is non empty RelStr
S is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
X is non empty full SubRelStr of T
the carrier of X is non empty set
Y is non empty full SubRelStr of S
the carrier of Y is non empty set
K22( the carrier of X) is non empty set
K22( the carrier of Y) is non empty set
F is Element of K22( the carrier of Y)
"\/" (F,S) is Element of the carrier of S
iN is Element of K22( the carrier of X)
"\/" (iN,T) is Element of the carrier of T
T is non empty RelStr
S is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
X is non empty full SubRelStr of T
the carrier of X is non empty set
Y is non empty full SubRelStr of S
the carrier of Y is non empty set
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K22(K23( the carrier of X, the carrier of X))
K23( the carrier of X, the carrier of X) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of X)) is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr
F is full SubRelStr of T
the carrier of F is set
the InternalRel of F is Relation-like the carrier of F -defined the carrier of F -valued Element of K22(K23( the carrier of F, the carrier of F))
K23( the carrier of F, the carrier of F) is Relation-like set
K22(K23( the carrier of F, the carrier of F)) is non empty set
RelStr(# the carrier of F, the InternalRel of F #) is strict RelStr
K22( the carrier of X) is non empty set
K22( the carrier of Y) is non empty set
iN is directed Element of K22( the carrier of Y)
"\/" (iN,S) is Element of the carrier of S
jN is directed Element of K22( the carrier of X)
"\/" (jN,T) is Element of the carrier of T
T is non empty RelStr
S is non empty RelStr
the carrier of T is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of S is non empty set
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
X is non empty full SubRelStr of T
the carrier of X is non empty set
Y is non empty full SubRelStr of S
the carrier of Y is non empty set
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K22(K23( the carrier of X, the carrier of X))
K23( the carrier of X, the carrier of X) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of X)) is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr
F is full SubRelStr of T
the carrier of F is set
the InternalRel of F is Relation-like the carrier of F -defined the carrier of F -valued Element of K22(K23( the carrier of F, the carrier of F))
K23( the carrier of F, the carrier of F) is Relation-like set
K22(K23( the carrier of F, the carrier of F)) is non empty set
RelStr(# the carrier of F, the InternalRel of F #) is strict RelStr
K22( the carrier of X) is non empty set
K22( the carrier of Y) is non empty set
iN is filtered Element of K22( the carrier of Y)
"/\" (iN,S) is Element of the carrier of S
jN is filtered Element of K22( the carrier of X)
"/\" (jN,T) is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
X is non empty transitive directed NetStr over T
Lim X is Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
[#] S is non empty non proper open closed dense non boundary Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
Y is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) Element of K22(K23( the carrier of T, the carrier of S))
Y .: (Lim X) is Element of K22( the carrier of S)
Y * X is non empty transitive strict directed NetStr over S
Lim (Y * X) is Element of K22( the carrier of S)
F is set
iN is Element of the carrier of S
jN is set
Y . jN is set
Xj is a_neighborhood of iN
Int Xj is open Element of K22( the carrier of S)
j is Element of the carrier of T
Y " (Int Xj) is Element of K22( the carrier of T)
the carrier of X is non empty set
j is Element of the carrier of X
the mapping of (Y * X) is Relation-like the carrier of (Y * X) -defined the carrier of S -valued Function-like non empty V29( the carrier of (Y * X), the carrier of S) Element of K22(K23( the carrier of (Y * X), the carrier of S))
the carrier of (Y * X) is non empty set
K23( the carrier of (Y * X), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (Y * X), the carrier of S)) is non empty set
the mapping of X is Relation-like the carrier of X -defined the carrier of T -valued Function-like non empty V29( the carrier of X, the carrier of T) Element of K22(K23( the carrier of X, the carrier of T))
K23( the carrier of X, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of T)) is non empty set
Y * the mapping of X is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of X, the carrier of S))
K23( the carrier of X, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of S)) is non empty set
the InternalRel of (Y * X) is Relation-like the carrier of (Y * X) -defined the carrier of (Y * X) -valued Element of K22(K23( the carrier of (Y * X), the carrier of (Y * X)))
K23( the carrier of (Y * X), the carrier of (Y * X)) is Relation-like non empty set
K22(K23( the carrier of (Y * X), the carrier of (Y * X))) is non empty set
RelStr(# the carrier of (Y * X), the InternalRel of (Y * X) #) is strict RelStr
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of K22(K23( the carrier of X, the carrier of X))
K23( the carrier of X, the carrier of X) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of X)) is non empty set
RelStr(# the carrier of X, the InternalRel of X #) is strict RelStr
G is Element of the carrier of (Y * X)
C is Element of the carrier of (Y * X)
(Y * X) . C is Element of the carrier of S
the mapping of (Y * X) . C is Element of the carrier of S
z is Element of the carrier of X
X . z is Element of the carrier of T
the mapping of X . z is Element of the carrier of T
Y . (X . z) is Element of the carrier of S
T is non empty RelStr
S is non empty NetStr over T
the carrier of S is non empty set
netmap (S,T) is Relation-like the carrier of S -defined the carrier of T -valued Function-like V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
the carrier of T is non empty set
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
X is Element of the carrier of S
Y is Element of the carrier of S
S . Y is Element of the carrier of T
the mapping of S . Y is Element of the carrier of T
S . X is Element of the carrier of T
the mapping of S . X is Element of the carrier of T
X is Element of the carrier of S
Y is Element of the carrier of S
(netmap (S,T)) . X is set
(netmap (S,T)) . Y is set
S . X is Element of the carrier of T
the mapping of S . X is Element of the carrier of T
(netmap (S,T)) . X is Element of the carrier of T
S . Y is Element of the carrier of T
the mapping of S . Y is Element of the carrier of T
(netmap (S,T)) . Y is Element of the carrier of T
F is Element of the carrier of T
iN is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
S is Element of the carrier of T
{S} is non empty finite Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
{S} opp+id is non empty reflexive strict NetStr over T
the carrier of ({S} opp+id) is non empty set
Y is Element of the carrier of ({S} opp+id)
F is Element of the carrier of ({S} opp+id)
iN is Element of the carrier of ({S} opp+id)
Y is Element of the carrier of ({S} opp+id)
F is Element of the carrier of ({S} opp+id)
Y is Element of the carrier of ({S} opp+id)
F is Element of the carrier of ({S} opp+id)
netmap (({S} opp+id),T) is Relation-like the carrier of ({S} opp+id) -defined the carrier of T -valued Function-like V29( the carrier of ({S} opp+id), the carrier of T) Element of K22(K23( the carrier of ({S} opp+id), the carrier of T))
K23( the carrier of ({S} opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of ({S} opp+id), the carrier of T)) is non empty set
the mapping of ({S} opp+id) is Relation-like the carrier of ({S} opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of ({S} opp+id), the carrier of T) Element of K22(K23( the carrier of ({S} opp+id), the carrier of T))
(netmap (({S} opp+id),T)) . Y is Element of the carrier of T
(netmap (({S} opp+id),T)) . F is Element of the carrier of T
Y is Element of the carrier of ({S} opp+id)
F is Element of the carrier of ({S} opp+id)
({S} opp+id) . F is Element of the carrier of T
the mapping of ({S} opp+id) is Relation-like the carrier of ({S} opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of ({S} opp+id), the carrier of T) Element of K22(K23( the carrier of ({S} opp+id), the carrier of T))
K23( the carrier of ({S} opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of ({S} opp+id), the carrier of T)) is non empty set
the mapping of ({S} opp+id) . F is Element of the carrier of T
({S} opp+id) . Y is Element of the carrier of T
the mapping of ({S} opp+id) . Y is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
the Element of the carrier of T is Element of the carrier of T
{ the Element of the carrier of T} is non empty finite Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
{ the Element of the carrier of T} opp+id is non empty reflexive transitive strict directed monotone antitone eventually-directed eventually-filtered NetStr over T
T is non empty RelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty Element of K22( the carrier of T)
S opp+id is non empty strict NetStr over T
the carrier of (S opp+id) is non empty set
X is Element of the carrier of (S opp+id)
Y is Element of the carrier of (S opp+id)
(S opp+id) . Y is Element of the carrier of T
the mapping of (S opp+id) is Relation-like the carrier of (S opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of (S opp+id), the carrier of T) Element of K22(K23( the carrier of (S opp+id), the carrier of T))
K23( the carrier of (S opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (S opp+id), the carrier of T)) is non empty set
the mapping of (S opp+id) . Y is Element of the carrier of T
(S opp+id) . X is Element of the carrier of T
the mapping of (S opp+id) . X is Element of the carrier of T
T ~ is non empty strict RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
RelStr(# the carrier of T,( the InternalRel of T ~) #) is strict RelStr
the carrier of (T ~) is non empty set
F is Element of the carrier of (T ~)
iN is Element of the carrier of (T ~)
~ iN is Element of the carrier of T
~ F is Element of the carrier of T
T is non empty reflexive RelStr
the carrier of T is non empty set
S is non empty reflexive RelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone Element of K22(K23( the carrier of T, the carrier of S))
Y is non empty antitone NetStr over T
X * Y is non empty strict NetStr over S
the carrier of (X * Y) is non empty set
F is Element of the carrier of (X * Y)
iN is Element of the carrier of (X * Y)
(X * Y) . iN is Element of the carrier of S
the mapping of (X * Y) is Relation-like the carrier of (X * Y) -defined the carrier of S -valued Function-like non empty V29( the carrier of (X * Y), the carrier of S) Element of K22(K23( the carrier of (X * Y), the carrier of S))
K23( the carrier of (X * Y), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (X * Y), the carrier of S)) is non empty set
the mapping of (X * Y) . iN is Element of the carrier of S
(X * Y) . F is Element of the carrier of S
the mapping of (X * Y) . F is Element of the carrier of S
the carrier of Y is non empty set
the mapping of Y is Relation-like the carrier of Y -defined the carrier of T -valued Function-like non empty V29( the carrier of Y, the carrier of T) Element of K22(K23( the carrier of Y, the carrier of T))
K23( the carrier of Y, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of T)) is non empty set
X * the mapping of Y is Relation-like the carrier of Y -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of Y, the carrier of S))
K23( the carrier of Y, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of S)) is non empty set
the InternalRel of (X * Y) is Relation-like the carrier of (X * Y) -defined the carrier of (X * Y) -valued Element of K22(K23( the carrier of (X * Y), the carrier of (X * Y)))
K23( the carrier of (X * Y), the carrier of (X * Y)) is Relation-like non empty set
K22(K23( the carrier of (X * Y), the carrier of (X * Y))) is non empty set
RelStr(# the carrier of (X * Y), the InternalRel of (X * Y) #) is strict RelStr
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr
jN is Element of the carrier of Y
j is Element of the carrier of Y
Y . j is Element of the carrier of T
the mapping of Y . j is Element of the carrier of T
Y . jN is Element of the carrier of T
the mapping of Y . jN is Element of the carrier of T
X . (Y . j) is Element of the carrier of S
X . (Y . jN) is Element of the carrier of S
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty transitive directed NetStr over T
the carrier of S is non empty set
{ ("/\" ( { (S . b₂) where b₂ is Element of the carrier of S : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of S : verum } is set
Y is set
F is Element of the carrier of S
{ (S . b₁) where b₁ is Element of the carrier of S : F <= b₁ } is set
"/\" ( { (S . b₁) where b₁ is Element of the carrier of S : F <= b₁ } ,T) is Element of the carrier of T
Y is Element of K22( the carrier of T)
T is non empty reflexive transitive antisymmetric RelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty reflexive transitive directed monotone eventually-directed NetStr over T
the carrier of S is non empty set
{ ("/\" ( { (S . b₂) where b₂ is Element of the carrier of S : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of S : verum } is set
the Element of the carrier of S is Element of the carrier of S
{ (S . b₁) where b₁ is Element of the carrier of S : the Element of the carrier of S <= b₁ } is set
"/\" ( { (S . b₁) where b₁ is Element of the carrier of S : the Element of the carrier of S <= b₁ } ,T) is Element of the carrier of T
F is set
iN is Element of the carrier of S
{ (S . b₁) where b₁ is Element of the carrier of S : iN <= b₁ } is set
"/\" ( { (S . b₁) where b₁ is Element of the carrier of S : iN <= b₁ } ,T) is Element of the carrier of T
F is non empty Element of K22( the carrier of T)
iN is Element of the carrier of T
jN is Element of the carrier of T
j is Element of the carrier of S
{ (S . b₁) where b₁ is Element of the carrier of S : j <= b₁ } is set
"/\" ( { (S . b₁) where b₁ is Element of the carrier of S : j <= b₁ } ,T) is Element of the carrier of T
Xj is Element of the carrier of S
{ (S . b₁) where b₁ is Element of the carrier of S : Xj <= b₁ } is set
"/\" ( { (S . b₁) where b₁ is Element of the carrier of S : Xj <= b₁ } ,T) is Element of the carrier of T
[#] S is non empty non proper lower upper Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
j is Element of the carrier of S
G is Element of the carrier of S
C is Element of the carrier of S
{ (S . b₁) where b₁ is Element of the carrier of S : C <= b₁ } is set
"/\" ( { (S . b₁) where b₁ is Element of the carrier of S : C <= b₁ } ,T) is Element of the carrier of T
{ (S . b₁) where b₁ is Element of the carrier of S : a₁ <= b₁ } is set
k is Element of the carrier of S
{ (S . b₁) where b₁ is Element of the carrier of S : k <= b₁ } is set
S . k is Element of the carrier of T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S . k is Element of the carrier of T
fp is Element of the carrier of S
k is Element of the carrier of T
k is Element of the carrier of T
c₁₈ is Element of the carrier of S
S . c₁₈ is Element of the carrier of T
the mapping of S . c₁₈ is Element of the carrier of T
k is Element of the carrier of T
k is Element of the carrier of T
{ (S . b₁) where b₁ is Element of the carrier of S : j <= b₁ } is set
{ (S . b₁) where b₁ is Element of the carrier of S : G <= b₁ } is set
fp is set
k is Element of the carrier of S
S . k is Element of the carrier of T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S . k is Element of the carrier of T
k is Element of the carrier of S
fp is set
k is Element of the carrier of S
S . k is Element of the carrier of T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S . k is Element of the carrier of T
k is Element of the carrier of S
T is non empty 1-sorted
the carrier of T is non empty set
S is non empty NetStr over T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
the carrier of S is non empty set
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
rng the mapping of S is non empty Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
X is set
the Element of the carrier of S is Element of the carrier of S
F is Element of the carrier of S
S . F is Element of the carrier of T
the mapping of S . F is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima RelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty filtered Element of K22( the carrier of T)
S opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over T
lim_inf (S opp+id) is Element of the carrier of T
"/\" (S,T) is Element of the carrier of T
the carrier of (S opp+id) is non empty set
{ ((S opp+id) . b₁) where b₁ is Element of the carrier of (S opp+id) : a₁ <= b₁ } is set
"/\" ( { ((S opp+id) . b₁) where b₁ is Element of the carrier of (S opp+id) : a₁ <= b₁ } ,T) is Element of the carrier of T
Y is Element of the carrier of (S opp+id)
{ ((S opp+id) . b₁) where b₁ is Element of the carrier of (S opp+id) : Y <= b₁ } is set
"/\" ( { ((S opp+id) . b₁) where b₁ is Element of the carrier of (S opp+id) : Y <= b₁ } ,T) is Element of the carrier of T
j is set
Xj is Element of the carrier of (S opp+id)
(S opp+id) . Xj is Element of the carrier of T
the mapping of (S opp+id) is Relation-like the carrier of (S opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of (S opp+id), the carrier of T) Element of K22(K23( the carrier of (S opp+id), the carrier of T))
K23( the carrier of (S opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (S opp+id), the carrier of T)) is non empty set
the mapping of (S opp+id) . Xj is Element of the carrier of T
j is Element of the carrier of (S opp+id)
jN is Element of the carrier of (S opp+id)
(S opp+id) . Y is Element of the carrier of T
the mapping of (S opp+id) is Relation-like the carrier of (S opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of (S opp+id), the carrier of T) Element of K22(K23( the carrier of (S opp+id), the carrier of T))
K23( the carrier of (S opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (S opp+id), the carrier of T)) is non empty set
the mapping of (S opp+id) . Y is Element of the carrier of T
j is non empty Element of K22( the carrier of T)
"/\" (j,T) is Element of the carrier of T
Xj is Element of the carrier of T
iN is Element of the carrier of T
j is Element of the carrier of T
T ~ is non empty strict reflexive transitive antisymmetric RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
RelStr(# the carrier of T,( the InternalRel of T ~) #) is strict RelStr
iN ~ is Element of the carrier of (T ~)
the carrier of (T ~) is non empty set
j ~ is Element of the carrier of (T ~)
G is Element of the carrier of (S opp+id)
(S opp+id) . G is Element of the carrier of T
the mapping of (S opp+id) . G is Element of the carrier of T
{j} is non empty finite Element of K22( the carrier of T)
"/\" ({j},T) is Element of the carrier of T
{ H₁(b₁) where b₁ is Element of the carrier of (S opp+id) : S₁[b₁] } is set
{ H₂(b₁) where b₁ is Element of the carrier of (S opp+id) : S₁[b₁] } is set
{ ("/\" (S,T)) where b₁ is Element of the carrier of (S opp+id) : S₁[b₁] } is set
{("/\" (S,T))} is non empty finite Element of K22( the carrier of T)
"\/" ({("/\" (S,T))},T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima RelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty reflexive transitive antisymmetric lower-bounded /\-complete with_infima RelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
X is non empty filtered Element of K22( the carrier of T)
X opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over T
Y is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone Element of K22(K23( the carrier of T, the carrier of S))
Y * (X opp+id) is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over S
lim_inf (Y * (X opp+id)) is Element of the carrier of S
Y .: X is non empty Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
"/\" ((Y .: X),S) is Element of the carrier of S
the carrier of (Y * (X opp+id)) is non empty set
{ ((Y * (X opp+id)) . b₁) where b₁ is Element of the carrier of (Y * (X opp+id)) : a₁ <= b₁ } is set
the InternalRel of (Y * (X opp+id)) is Relation-like the carrier of (Y * (X opp+id)) -defined the carrier of (Y * (X opp+id)) -valued Element of K22(K23( the carrier of (Y * (X opp+id)), the carrier of (Y * (X opp+id))))
K23( the carrier of (Y * (X opp+id)), the carrier of (Y * (X opp+id))) is Relation-like non empty set
K22(K23( the carrier of (Y * (X opp+id)), the carrier of (Y * (X opp+id)))) is non empty set
RelStr(# the carrier of (Y * (X opp+id)), the InternalRel of (Y * (X opp+id)) #) is strict RelStr
the carrier of (X opp+id) is non empty set
the InternalRel of (X opp+id) is Relation-like the carrier of (X opp+id) -defined the carrier of (X opp+id) -valued Element of K22(K23( the carrier of (X opp+id), the carrier of (X opp+id)))
K23( the carrier of (X opp+id), the carrier of (X opp+id)) is Relation-like non empty set
K22(K23( the carrier of (X opp+id), the carrier of (X opp+id))) is non empty set
RelStr(# the carrier of (X opp+id), the InternalRel of (X opp+id) #) is strict RelStr
the mapping of (Y * (X opp+id)) is Relation-like the carrier of (Y * (X opp+id)) -defined the carrier of S -valued Function-like non empty V29( the carrier of (Y * (X opp+id)), the carrier of S) Element of K22(K23( the carrier of (Y * (X opp+id)), the carrier of S))
K23( the carrier of (Y * (X opp+id)), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (Y * (X opp+id)), the carrier of S)) is non empty set
the mapping of (X opp+id) is Relation-like the carrier of (X opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of (X opp+id), the carrier of T) Element of K22(K23( the carrier of (X opp+id), the carrier of T))
K23( the carrier of (X opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (X opp+id), the carrier of T)) is non empty set
Y * the mapping of (X opp+id) is Relation-like the carrier of (X opp+id) -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of (X opp+id), the carrier of S))
K23( the carrier of (X opp+id), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (X opp+id), the carrier of S)) is non empty set
id X is Relation-like X -defined X -valued Function-like one-to-one non empty V24(X) Element of K22(K23(X,X))
K23(X,X) is Relation-like non empty set
K22(K23(X,X)) is non empty set
jN is Element of the carrier of (Y * (X opp+id))
{ ((Y * (X opp+id)) . b₁) where b₁ is Element of the carrier of (Y * (X opp+id)) : jN <= b₁ } is set
"/\" (H₁(jN),S) is Element of the carrier of S
[#] (Y * (X opp+id)) is non empty non proper lower upper Element of K22( the carrier of (Y * (X opp+id)))
K22( the carrier of (Y * (X opp+id))) is non empty set
j is Element of the carrier of (Y * (X opp+id))
Xj is Element of the carrier of (Y * (X opp+id))
{ ((Y * (X opp+id)) . b₁) where b₁ is Element of the carrier of (Y * (X opp+id)) : j <= b₁ } is set
j is set
G is Element of the carrier of (Y * (X opp+id))
(Y * (X opp+id)) . G is Element of the carrier of S
the mapping of (Y * (X opp+id)) . G is Element of the carrier of S
C is Element of the carrier of (Y * (X opp+id))
(Y * (X opp+id)) . C is Element of the carrier of S
the mapping of (Y * (X opp+id)) . C is Element of the carrier of S
(id X) . C is set
Y . ((id X) . C) is set
z is Element of the carrier of (X opp+id)
Y . z is set
(Y * (X opp+id)) . Xj is Element of the carrier of S
the mapping of (Y * (X opp+id)) . Xj is Element of the carrier of S
"/\" (H₁(j),S) is Element of the carrier of S
j is Element of the carrier of S
G is set
Y . G is set
C is Element of the carrier of (Y * (X opp+id))
z is Element of the carrier of (Y * (X opp+id))
T ~ is non empty strict reflexive transitive antisymmetric RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
RelStr(# the carrier of T,( the InternalRel of T ~) #) is strict RelStr
fp is Element of the carrier of T
fp ~ is Element of the carrier of (T ~)
the carrier of (T ~) is non empty set
k is Element of the carrier of T
k ~ is Element of the carrier of (T ~)
Y . k is Element of the carrier of S
(Y * (X opp+id)) . z is Element of the carrier of S
the mapping of (Y * (X opp+id)) . z is Element of the carrier of S
(id X) . z is set
Y . ((id X) . z) is set
{ H₂(b₁) where b₁ is Element of the carrier of (Y * (X opp+id)) : S₁[b₁] } is set
{ H₃(b₁) where b₁ is Element of the carrier of (Y * (X opp+id)) : S₁[b₁] } is set
{ ("/\" ((Y .: X),S)) where b₁ is Element of the carrier of (Y * (X opp+id)) : S₁[b₁] } is set
{("/\" ((Y .: X),S))} is non empty finite Element of K22( the carrier of S)
"\/" ({("/\" ((Y .: X),S))},S) is Element of the carrier of S
T is non empty TopSpace-like reflexive transitive antisymmetric TopRelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric TopRelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
K22( the carrier of S) is non empty set
X is non empty filtered Element of K22( the carrier of T)
X opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over T
Y is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone Element of K22(K23( the carrier of T, the carrier of S))
Y .: X is non empty Element of K22( the carrier of S)
Y * (X opp+id) is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over S
F is non empty filtered Element of K22( the carrier of S)
F opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over S
the carrier of (Y * (X opp+id)) is non empty set
the InternalRel of (Y * (X opp+id)) is Relation-like the carrier of (Y * (X opp+id)) -defined the carrier of (Y * (X opp+id)) -valued Element of K22(K23( the carrier of (Y * (X opp+id)), the carrier of (Y * (X opp+id))))
K23( the carrier of (Y * (X opp+id)), the carrier of (Y * (X opp+id))) is Relation-like non empty set
K22(K23( the carrier of (Y * (X opp+id)), the carrier of (Y * (X opp+id)))) is non empty set
RelStr(# the carrier of (Y * (X opp+id)), the InternalRel of (Y * (X opp+id)) #) is strict RelStr
the carrier of (X opp+id) is non empty set
the InternalRel of (X opp+id) is Relation-like the carrier of (X opp+id) -defined the carrier of (X opp+id) -valued Element of K22(K23( the carrier of (X opp+id), the carrier of (X opp+id)))
K23( the carrier of (X opp+id), the carrier of (X opp+id)) is Relation-like non empty set
K22(K23( the carrier of (X opp+id), the carrier of (X opp+id))) is non empty set
RelStr(# the carrier of (X opp+id), the InternalRel of (X opp+id) #) is strict RelStr
the mapping of (Y * (X opp+id)) is Relation-like the carrier of (Y * (X opp+id)) -defined the carrier of S -valued Function-like non empty V29( the carrier of (Y * (X opp+id)), the carrier of S) Element of K22(K23( the carrier of (Y * (X opp+id)), the carrier of S))
K23( the carrier of (Y * (X opp+id)), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (Y * (X opp+id)), the carrier of S)) is non empty set
the mapping of (X opp+id) is Relation-like the carrier of (X opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of (X opp+id), the carrier of T) Element of K22(K23( the carrier of (X opp+id), the carrier of T))
K23( the carrier of (X opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (X opp+id), the carrier of T)) is non empty set
Y * the mapping of (X opp+id) is Relation-like the carrier of (X opp+id) -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of (X opp+id), the carrier of S))
K23( the carrier of (X opp+id), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (X opp+id), the carrier of S)) is non empty set
the carrier of (F opp+id) is non empty set
the mapping of (F opp+id) is Relation-like the carrier of (F opp+id) -defined the carrier of S -valued Function-like non empty V29( the carrier of (F opp+id), the carrier of S) Element of K22(K23( the carrier of (F opp+id), the carrier of S))
K23( the carrier of (F opp+id), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (F opp+id), the carrier of S)) is non empty set
id F is Relation-like F -defined F -valued Function-like one-to-one non empty V24(F) Element of K22(K23(F,F))
K23(F,F) is Relation-like non empty set
K22(K23(F,F)) is non empty set
id X is Relation-like X -defined X -valued Function-like one-to-one non empty V24(X) Element of K22(K23(X,X))
K23(X,X) is Relation-like non empty set
K22(K23(X,X)) is non empty set
Y | X is Relation-like the carrier of T -defined X -defined the carrier of T -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of T, the carrier of S))
rng the mapping of (Y * (X opp+id)) is non empty Element of K22( the carrier of S)
dom the mapping of (Y * (X opp+id)) is non empty Element of K22( the carrier of (Y * (X opp+id)))
K22( the carrier of (Y * (X opp+id))) is non empty set
K23( the carrier of (Y * (X opp+id)), the carrier of (F opp+id)) is Relation-like non empty set
K22(K23( the carrier of (Y * (X opp+id)), the carrier of (F opp+id))) is non empty set
j is Relation-like the carrier of (Y * (X opp+id)) -defined the carrier of (F opp+id) -valued Function-like V29( the carrier of (Y * (X opp+id)), the carrier of (F opp+id)) Element of K22(K23( the carrier of (Y * (X opp+id)), the carrier of (F opp+id)))
the mapping of (F opp+id) * j is Relation-like the carrier of (Y * (X opp+id)) -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of (Y * (X opp+id)), the carrier of S))
Xj is Element of the carrier of (F opp+id)
j is set
Y . j is set
G is Element of the carrier of (Y * (X opp+id))
C is Element of the carrier of (Y * (X opp+id))
j . C is Element of the carrier of (F opp+id)
k is Element of the carrier of T
Y . k is Element of the carrier of S
T ~ is non empty strict reflexive transitive antisymmetric RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
RelStr(# the carrier of T,( the InternalRel of T ~) #) is strict RelStr
S ~ is non empty strict reflexive transitive antisymmetric RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
the InternalRel of S ~ is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
RelStr(# the carrier of S,( the InternalRel of S ~) #) is strict RelStr
z is Element of the carrier of T
z ~ is Element of the carrier of (T ~)
the carrier of (T ~) is non empty set
k ~ is Element of the carrier of (T ~)
Y . z is Element of the carrier of S
(Y . z) ~ is Element of the carrier of (S ~)
the carrier of (S ~) is non empty set
(Y . k) ~ is Element of the carrier of (S ~)
fp is Element of the carrier of (F opp+id)
T is non empty TopSpace-like reflexive transitive antisymmetric TopRelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty TopSpace-like reflexive transitive antisymmetric TopRelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
K22( the carrier of S) is non empty set
X is non empty filtered Element of K22( the carrier of T)
X opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over T
Y is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone Element of K22(K23( the carrier of T, the carrier of S))
Y .: X is non empty Element of K22( the carrier of S)
Y * (X opp+id) is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over S
Lim (Y * (X opp+id)) is Element of K22( the carrier of S)
F is non empty filtered Element of K22( the carrier of S)
F opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over S
Lim (F opp+id) is Element of K22( the carrier of S)
T is non empty reflexive RelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty Element of K22( the carrier of T)
Net-Str S is strict NetStr over T
the mapping of (Net-Str S) is Relation-like the carrier of (Net-Str S) -defined the carrier of T -valued Function-like V29( the carrier of (Net-Str S), the carrier of T) Element of K22(K23( the carrier of (Net-Str S), the carrier of T))
the carrier of (Net-Str S) is set
K23( the carrier of (Net-Str S), the carrier of T) is Relation-like set
K22(K23( the carrier of (Net-Str S), the carrier of T)) is non empty set
id S is Relation-like S -defined S -valued Function-like one-to-one non empty V24(S) Element of K22(K23(S,S))
K23(S,S) is Relation-like non empty set
K22(K23(S,S)) is non empty set
dom (id S) is non empty Element of K22(S)
K22(S) is non empty set
rng (id S) is non empty Element of K22(S)
K23(S, the carrier of T) is Relation-like non empty set
K22(K23(S, the carrier of T)) is non empty set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
(id the carrier of T) | S is Relation-like the carrier of T -defined S -defined the carrier of T -defined the carrier of T -valued Function-like Element of K22(K23( the carrier of T, the carrier of T))
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
the InternalRel of T |_2 S is Relation-like S -defined S -valued Element of K22(K23(S,S))
the InternalRel of T /\ K23(S,S) is Relation-like the carrier of T -defined the carrier of T -valued set
Y is Relation-like S -defined the carrier of T -valued Function-like V29(S, the carrier of T) Element of K22(K23(S, the carrier of T))
NetStr(# S,( the InternalRel of T |_2 S),Y #) is non empty strict NetStr over T
the InternalRel of (Net-Str S) is Relation-like the carrier of (Net-Str S) -defined the carrier of (Net-Str S) -valued Element of K22(K23( the carrier of (Net-Str S), the carrier of (Net-Str S)))
K23( the carrier of (Net-Str S), the carrier of (Net-Str S)) is Relation-like set
K22(K23( the carrier of (Net-Str S), the carrier of (Net-Str S))) is non empty set
T is non empty reflexive transitive antisymmetric up-complete RelStr
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric up-complete RelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
K22( the carrier of T) is non empty set
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone Element of K22(K23( the carrier of T, the carrier of S))
Y is non empty directed Element of K22( the carrier of T)
Net-Str Y is non empty reflexive transitive strict directed monotone eventually-directed NetStr over T
X * (Net-Str Y) is non empty reflexive transitive strict directed NetStr over S
lim_inf (X * (Net-Str Y)) is Element of the carrier of S
X .: Y is non empty Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
"\/" ((X .: Y),S) is Element of the carrier of S
the carrier of (X * (Net-Str Y)) is non empty set
{ ((X * (Net-Str Y)) . b₁) where b₁ is Element of the carrier of (X * (Net-Str Y)) : a₁ <= b₁ } is set
{ H₂(b₁) where b₁ is Element of the carrier of (X * (Net-Str Y)) : verum } is set
the InternalRel of (X * (Net-Str Y)) is Relation-like the carrier of (X * (Net-Str Y)) -defined the carrier of (X * (Net-Str Y)) -valued Element of K22(K23( the carrier of (X * (Net-Str Y)), the carrier of (X * (Net-Str Y))))
K23( the carrier of (X * (Net-Str Y)), the carrier of (X * (Net-Str Y))) is Relation-like non empty set
K22(K23( the carrier of (X * (Net-Str Y)), the carrier of (X * (Net-Str Y)))) is non empty set
RelStr(# the carrier of (X * (Net-Str Y)), the InternalRel of (X * (Net-Str Y)) #) is strict RelStr
the carrier of (Net-Str Y) is non empty set
the InternalRel of (Net-Str Y) is Relation-like the carrier of (Net-Str Y) -defined the carrier of (Net-Str Y) -valued Element of K22(K23( the carrier of (Net-Str Y), the carrier of (Net-Str Y)))
K23( the carrier of (Net-Str Y), the carrier of (Net-Str Y)) is Relation-like non empty set
K22(K23( the carrier of (Net-Str Y), the carrier of (Net-Str Y))) is non empty set
RelStr(# the carrier of (Net-Str Y), the InternalRel of (Net-Str Y) #) is strict RelStr
the mapping of (X * (Net-Str Y)) is Relation-like the carrier of (X * (Net-Str Y)) -defined the carrier of S -valued Function-like non empty V29( the carrier of (X * (Net-Str Y)), the carrier of S) Element of K22(K23( the carrier of (X * (Net-Str Y)), the carrier of S))
K23( the carrier of (X * (Net-Str Y)), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (X * (Net-Str Y)), the carrier of S)) is non empty set
the mapping of (Net-Str Y) is Relation-like the carrier of (Net-Str Y) -defined the carrier of T -valued Function-like non empty V29( the carrier of (Net-Str Y), the carrier of T) Element of K22(K23( the carrier of (Net-Str Y), the carrier of T))
K23( the carrier of (Net-Str Y), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (Net-Str Y), the carrier of T)) is non empty set
X * the mapping of (Net-Str Y) is Relation-like the carrier of (Net-Str Y) -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of (Net-Str Y), the carrier of S))
K23( the carrier of (Net-Str Y), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (Net-Str Y), the carrier of S)) is non empty set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one non empty V24(Y) Element of K22(K23(Y,Y))
K23(Y,Y) is Relation-like non empty set
K22(K23(Y,Y)) is non empty set
j is Element of the carrier of (X * (Net-Str Y))
(X * (Net-Str Y)) . j is Element of the carrier of S
the mapping of (X * (Net-Str Y)) . j is Element of the carrier of S
(id Y) . j is set
X . ((id Y) . j) is set
X . j is set
j is Element of the carrier of (X * (Net-Str Y))
{ ((X * (Net-Str Y)) . b₁) where b₁ is Element of the carrier of (X * (Net-Str Y)) : j <= b₁ } is set
"/\" (H₁(j),S) is Element of the carrier of S
X . j is set
(X * (Net-Str Y)) . j is Element of the carrier of S
the mapping of (X * (Net-Str Y)) . j is Element of the carrier of S
Xj is Element of the carrier of T
X . Xj is Element of the carrier of S
j is Element of the carrier of S
j is Element of the carrier of S
G is Element of the carrier of (X * (Net-Str Y))
(X * (Net-Str Y)) . G is Element of the carrier of S
the mapping of (X * (Net-Str Y)) . G is Element of the carrier of S
C is Element of the carrier of (X * (Net-Str Y))
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
z is Element of the carrier of T
X . z is Element of the carrier of S
j is set
Xj is Element of the carrier of (X * (Net-Str Y))
{ ((X * (Net-Str Y)) . b₁) where b₁ is Element of the carrier of (X * (Net-Str Y)) : Xj <= b₁ } is set
"/\" (H₁(Xj),S) is Element of the carrier of S
j is Element of the carrier of (X * (Net-Str Y))
X . j is set
j is set
Xj is set
X . Xj is set
j is Element of the carrier of T
X . j is Element of the carrier of S
G is Element of the carrier of (X * (Net-Str Y))
{ ((X * (Net-Str Y)) . b₁) where b₁ is Element of the carrier of (X * (Net-Str Y)) : G <= b₁ } is set
"/\" (H₁(G),S) is Element of the carrier of S
T is non empty reflexive RelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty directed Element of K22( the carrier of T)
Net-Str S is non empty reflexive strict directed monotone eventually-directed NetStr over T
the carrier of (Net-Str S) is non empty set
id S is Relation-like S -defined S -valued Function-like one-to-one non empty V24(S) Element of K22(K23(S,S))
K23(S,S) is Relation-like non empty set
K22(K23(S,S)) is non empty set
dom (id S) is non empty Element of K22(S)
K22(S) is non empty set
rng (id S) is non empty Element of K22(S)
K23(S, the carrier of T) is Relation-like non empty set
K22(K23(S, the carrier of T)) is non empty set
id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V24( the carrier of T) Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
(id the carrier of T) | S is Relation-like the carrier of T -defined S -defined the carrier of T -defined the carrier of T -valued Function-like Element of K22(K23( the carrier of T, the carrier of T))
X is Relation-like S -defined the carrier of T -valued Function-like V29(S, the carrier of T) Element of K22(K23(S, the carrier of T))
Net-Str (S,X) is non empty strict NetStr over T
Y is Element of the carrier of (Net-Str S)
F is Element of the carrier of (Net-Str S)
(Net-Str S) . Y is Element of the carrier of T
the mapping of (Net-Str S) is Relation-like the carrier of (Net-Str S) -defined the carrier of T -valued Function-like non empty V29( the carrier of (Net-Str S), the carrier of T) Element of K22(K23( the carrier of (Net-Str S), the carrier of T))
K23( the carrier of (Net-Str S), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (Net-Str S), the carrier of T)) is non empty set
the mapping of (Net-Str S) . Y is Element of the carrier of T
(Net-Str S) . F is Element of the carrier of T
the mapping of (Net-Str S) . F is Element of the carrier of T
iN is Element of the carrier of (Net-Str S)
(Net-Str S) . iN is Element of the carrier of T
the mapping of (Net-Str S) . iN is Element of the carrier of T
jN is Element of the carrier of (Net-Str S)
(Net-Str S) . jN is Element of the carrier of T
the mapping of (Net-Str S) . jN is Element of the carrier of T
T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty directed Element of K22( the carrier of T)
"\/" (S,T) is Element of the carrier of T
Net-Str S is non empty reflexive transitive strict directed monotone eventually-directed NetStr over T
Lim (Net-Str S) is Element of K22( the carrier of T)
the mapping of (Net-Str S) is Relation-like the carrier of (Net-Str S) -defined the carrier of T -valued Function-like non empty V29( the carrier of (Net-Str S), the carrier of T) Element of K22(K23( the carrier of (Net-Str S), the carrier of T))
the carrier of (Net-Str S) is non empty set
K23( the carrier of (Net-Str S), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (Net-Str S), the carrier of T)) is non empty set
id S is Relation-like S -defined S -valued Function-like one-to-one non empty V24(S) Element of K22(K23(S,S))
K23(S,S) is Relation-like non empty set
K22(K23(S,S)) is non empty set
K22(K22( the carrier of T)) is non empty set
the quasi_prebasis V123(T) Element of K22(K22( the carrier of T)) is quasi_prebasis V123(T) Element of K22(K22( the carrier of T))
F is Element of K22( the carrier of T)
the topology of T is non empty Element of K22(K22( the carrier of T))
iN is Element of the carrier of T
jN is Element of the carrier of (Net-Str S)
j is Element of the carrier of (Net-Str S)
(Net-Str S) . j is Element of the carrier of T
the mapping of (Net-Str S) . j is Element of the carrier of T
(Net-Str S) . jN is Element of the carrier of T
the mapping of (Net-Str S) . jN is Element of the carrier of T
T is non empty 1-sorted
X is non empty NetStr over T
S is non empty transitive directed NetStr over T
the carrier of X is non empty set
the carrier of S is non empty set
K23( the carrier of X, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of S)) is non empty set
the carrier of T is non empty set
the mapping of X is Relation-like the carrier of X -defined the carrier of T -valued Function-like non empty V29( the carrier of X, the carrier of T) Element of K22(K23( the carrier of X, the carrier of T))
K23( the carrier of X, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of T)) is non empty set
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
T is non empty 1-sorted
S is non empty transitive directed NetStr over T
the carrier of S is non empty set
X is non empty transitive directed subnet of S
the carrier of X is non empty set
Y is Relation-like the carrier of X -defined the carrier of S -valued Function-like V29( the carrier of X, the carrier of S) (T,S,X)
F is Element of the carrier of X
X . F is Element of the carrier of T
the carrier of T is non empty set
the mapping of X is Relation-like the carrier of X -defined the carrier of T -valued Function-like non empty V29( the carrier of X, the carrier of T) Element of K22(K23( the carrier of X, the carrier of T))
K23( the carrier of X, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of T)) is non empty set
the mapping of X . F is Element of the carrier of T
Y . F is Element of the carrier of S
S . (Y . F) is Element of the carrier of T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S . (Y . F) is Element of the carrier of T
the mapping of S * Y is Relation-like the carrier of X -defined the carrier of T -valued Function-like Element of K22(K23( the carrier of X, the carrier of T))
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty transitive directed NetStr over T
lim_inf S is Element of the carrier of T
the carrier of T is non empty set
X is non empty transitive directed subnet of S
lim_inf X is Element of the carrier of T
{ ("/\" ( { (a₁ . b₂) where b₂ is Element of the carrier of a₁ : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of a₁ : verum } is set
the carrier of S is non empty set
{ ("/\" ( { (S . b₂) where b₂ is Element of the carrier of S : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of S : verum } is set
the carrier of X is non empty set
{ ("/\" ( { (X . b₂) where b₂ is Element of the carrier of X : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of X : verum } is set
"\/" (H₁(X),T) is Element of the carrier of T
Y is Element of the carrier of T
F is Element of the carrier of S
{ (S . b₁) where b₁ is Element of the carrier of S : F <= b₁ } is set
"/\" ( { (S . b₁) where b₁ is Element of the carrier of S : F <= b₁ } ,T) is Element of the carrier of T
the Relation-like the carrier of X -defined the carrier of S -valued Function-like V29( the carrier of X, the carrier of S) (T,S,X) is Relation-like the carrier of X -defined the carrier of S -valued Function-like V29( the carrier of X, the carrier of S) (T,S,X)
jN is Element of the carrier of S
j is Element of the carrier of X
{ (S . b₁) where b₁ is Element of the carrier of S : jN <= b₁ } is set
{ (X . b₁) where b₁ is Element of the carrier of X : j <= b₁ } is set
G is set
C is Element of the carrier of X
X . C is Element of the carrier of T
the mapping of X is Relation-like the carrier of X -defined the carrier of T -valued Function-like non empty V29( the carrier of X, the carrier of T) Element of K22(K23( the carrier of X, the carrier of T))
K23( the carrier of X, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of T)) is non empty set
the mapping of X . C is Element of the carrier of T
z is Element of the carrier of X
the Relation-like the carrier of X -defined the carrier of S -valued Function-like V29( the carrier of X, the carrier of S) (T,S,X) . z is Element of the carrier of S
S . ( the Relation-like the carrier of X -defined the carrier of S -valued Function-like V29( the carrier of X, the carrier of S) (T,S,X) . z) is Element of the carrier of T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S . ( the Relation-like the carrier of X -defined the carrier of S -valued Function-like V29( the carrier of X, the carrier of S) (T,S,X) . z) is Element of the carrier of T
"/\" ( { (X . b₁) where b₁ is Element of the carrier of X : j <= b₁ } ,T) is Element of the carrier of T
"\/" (H₁(S),T) is Element of the carrier of T
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty transitive directed NetStr over T
the carrier of S is non empty set
lim_inf S is Element of the carrier of T
the carrier of T is non empty set
X is non empty transitive directed subnet of S
the carrier of X is non empty set
lim_inf X is Element of the carrier of T
Y is Relation-like the carrier of X -defined the carrier of S -valued Function-like V29( the carrier of X, the carrier of S) (T,S,X)
{ ("/\" ( { (a₁ . b₂) where b₂ is Element of the carrier of a₁ : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of a₁ : verum } is set
{ ("/\" ( { (X . b₂) where b₂ is Element of the carrier of X : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of X : verum } is set
{ ("/\" ( { (S . b₂) where b₂ is Element of the carrier of S : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of S : verum } is set
"\/" (H₁(S),T) is Element of the carrier of T
F is Element of the carrier of T
iN is Element of the carrier of X
{ (X . b₁) where b₁ is Element of the carrier of X : iN <= b₁ } is set
"/\" ( { (X . b₁) where b₁ is Element of the carrier of X : iN <= b₁ } ,T) is Element of the carrier of T
jN is Element of the carrier of X
Y . jN is Element of the carrier of S
{ (S . b₁) where b₁ is Element of the carrier of S : Y . jN <= b₁ } is set
{ (X . b₁) where b₁ is Element of the carrier of X : jN <= b₁ } is set
G is Element of the carrier of T
C is Element of the carrier of S
S . C is Element of the carrier of T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S . C is Element of the carrier of T
z is Element of the carrier of S
S . z is Element of the carrier of T
the mapping of S . z is Element of the carrier of T
k is Element of the carrier of X
X . k is Element of the carrier of T
the mapping of X is Relation-like the carrier of X -defined the carrier of T -valued Function-like non empty V29( the carrier of X, the carrier of T) Element of K22(K23( the carrier of X, the carrier of T))
K23( the carrier of X, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of T)) is non empty set
the mapping of X . k is Element of the carrier of T
"/\" ( { (S . b₁) where b₁ is Element of the carrier of S : Y . jN <= b₁ } ,T) is Element of the carrier of T
"\/" (H₁(X),T) is Element of the carrier of T
T is non empty RelStr
S is non empty transitive directed NetStr over T
the carrier of S is non empty set
X is non empty full SubNetStr of S
the carrier of X is non empty set
incl (X,S) is Relation-like the carrier of X -defined the carrier of S -valued Function-like V29( the carrier of X, the carrier of S) Element of K22(K23( the carrier of X, the carrier of S))
K23( the carrier of X, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of S)) is non empty set
the mapping of X is Relation-like the carrier of X -defined the carrier of T -valued Function-like non empty V29( the carrier of X, the carrier of T) Element of K22(K23( the carrier of X, the carrier of T))
the carrier of T is non empty set
K23( the carrier of X, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of T)) is non empty set
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S | the carrier of X is Relation-like the carrier of S -defined the carrier of X -defined the carrier of S -defined the carrier of T -valued Function-like Element of K22(K23( the carrier of S, the carrier of T))
Y is Element of the carrier of X
F is Element of the carrier of X
iN is Element of the carrier of S
jN is Element of the carrier of S
j is Element of the carrier of S
Xj is Element of the carrier of S
j is Element of the carrier of X
Y is non empty transitive directed NetStr over T
incl (Y,S) is Relation-like the carrier of Y -defined the carrier of S -valued Function-like V29( the carrier of Y, the carrier of S) Element of K22(K23( the carrier of Y, the carrier of S))
the carrier of Y is non empty set
K23( the carrier of Y, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of S)) is non empty set
id the carrier of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like one-to-one non empty V24( the carrier of Y) Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
the mapping of Y is Relation-like the carrier of Y -defined the carrier of T -valued Function-like non empty V29( the carrier of Y, the carrier of T) Element of K22(K23( the carrier of Y, the carrier of T))
K23( the carrier of Y, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of T)) is non empty set
the mapping of S * (incl (Y,S)) is Relation-like the carrier of Y -defined the carrier of T -valued Function-like Element of K22(K23( the carrier of Y, the carrier of T))
iN is Element of the carrier of S
jN is Element of the carrier of S
j is Element of the carrier of Y
j is Element of the carrier of Y
Xj is Element of the carrier of Y
G is Element of the carrier of S
(incl (Y,S)) . j is Element of the carrier of S
T is non empty RelStr
S is non empty transitive directed NetStr over T
the carrier of S is non empty set
X is Element of the carrier of S
S | X is non empty transitive strict directed subnet of S
incl ((S | X),S) is Relation-like the carrier of (S | X) -defined the carrier of S -valued Function-like V29( the carrier of (S | X), the carrier of S) Element of K22(K23( the carrier of (S | X), the carrier of S))
the carrier of (S | X) is non empty set
K23( the carrier of (S | X), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (S | X), the carrier of S)) is non empty set
the carrier of T is non empty set
the mapping of (S | X) is Relation-like the carrier of (S | X) -defined the carrier of T -valued Function-like non empty V29( the carrier of (S | X), the carrier of T) Element of K22(K23( the carrier of (S | X), the carrier of T))
K23( the carrier of (S | X), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (S | X), the carrier of T)) is non empty set
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S * (incl ((S | X),S)) is Relation-like the carrier of (S | X) -defined the carrier of T -valued Function-like Element of K22(K23( the carrier of (S | X), the carrier of T))
id the carrier of (S | X) is Relation-like the carrier of (S | X) -defined the carrier of (S | X) -valued Function-like one-to-one non empty V24( the carrier of (S | X)) Element of K22(K23( the carrier of (S | X), the carrier of (S | X)))
K23( the carrier of (S | X), the carrier of (S | X)) is Relation-like non empty set
K22(K23( the carrier of (S | X), the carrier of (S | X))) is non empty set
the mapping of S | the carrier of (S | X) is Relation-like the carrier of S -defined the carrier of (S | X) -defined the carrier of S -defined the carrier of T -valued Function-like Element of K22(K23( the carrier of S, the carrier of T))
iN is Element of the carrier of S
jN is Element of the carrier of S
j is Element of the carrier of (S | X)
Xj is Element of the carrier of (S | X)
(incl ((S | X),S)) . Xj is Element of the carrier of S
j is Element of the carrier of S
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete RelStr
S is non empty transitive directed NetStr over T
the carrier of S is non empty set
lim_inf S is Element of the carrier of T
the carrier of T is non empty set
X is Element of the carrier of S
S | X is non empty transitive strict directed subnet of S
lim_inf (S | X) is Element of the carrier of T
Y is non empty transitive directed subnet of S
the carrier of Y is non empty set
incl (Y,S) is Relation-like the carrier of Y -defined the carrier of S -valued Function-like V29( the carrier of Y, the carrier of S) Element of K22(K23( the carrier of Y, the carrier of S))
K23( the carrier of Y, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of S)) is non empty set
id the carrier of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Function-like one-to-one non empty V24( the carrier of Y) Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
jN is Element of the carrier of Y
j is Element of the carrier of S
F is Relation-like the carrier of Y -defined the carrier of S -valued Function-like V29( the carrier of Y, the carrier of S) (T,S,Y)
F . jN is Element of the carrier of S
iN is Element of the carrier of S
Xj is Element of the carrier of Y
j is Element of the carrier of Y
Y . j is Element of the carrier of T
the mapping of Y is Relation-like the carrier of Y -defined the carrier of T -valued Function-like non empty V29( the carrier of Y, the carrier of T) Element of K22(K23( the carrier of Y, the carrier of T))
K23( the carrier of Y, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of T)) is non empty set
the mapping of Y . j is Element of the carrier of T
F . j is Element of the carrier of S
S . (F . j) is Element of the carrier of T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S . (F . j) is Element of the carrier of T
S . iN is Element of the carrier of T
the mapping of S . iN is Element of the carrier of T
T is non empty RelStr
the carrier of T is non empty set
S is non empty transitive directed NetStr over T
the carrier of S is non empty set
X is set
Y is Element of the carrier of S
[#] S is non empty non proper lower upper Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
F is Element of the carrier of S
S . F is Element of the carrier of T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
the mapping of S . F is Element of the carrier of T
S | F is non empty transitive strict directed subnet of S
the mapping of (S | F) is Relation-like the carrier of (S | F) -defined the carrier of T -valued Function-like non empty V29( the carrier of (S | F), the carrier of T) Element of K22(K23( the carrier of (S | F), the carrier of T))
the carrier of (S | F) is non empty set
K23( the carrier of (S | F), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (S | F), the carrier of T)) is non empty set
rng the mapping of (S | F) is non empty Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
iN is set
dom the mapping of (S | F) is non empty Element of K22( the carrier of (S | F))
K22( the carrier of (S | F)) is non empty set
jN is set
the mapping of (S | F) . jN is set
{ b₁ where b₁ is Element of the carrier of S : F <= b₁ } is set
j is Element of the carrier of (S | F)
Xj is Element of the carrier of S
(S | F) . j is Element of the carrier of T
the mapping of (S | F) . j is Element of the carrier of T
S . Xj is Element of the carrier of T
the mapping of S . Xj is Element of the carrier of T
T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty transitive directed eventually-filtered NetStr over T
the mapping of S is Relation-like the carrier of S -defined the carrier of T -valued Function-like non empty V29( the carrier of S, the carrier of T) Element of K22(K23( the carrier of S, the carrier of T))
the carrier of S is non empty set
K23( the carrier of S, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of T)) is non empty set
rng the mapping of S is non empty Element of K22( the carrier of T)
X is non empty Element of K22( the carrier of T)
Y is Element of the carrier of T
F is Element of the carrier of T
dom the mapping of S is non empty Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
iN is set
the mapping of S . iN is set
jN is set
the mapping of S . jN is set
j is Element of the carrier of S
S . j is Element of the carrier of T
the mapping of S . j is Element of the carrier of T
j is Element of the carrier of S
Xj is Element of the carrier of S
S . Xj is Element of the carrier of T
the mapping of S . Xj is Element of the carrier of T
G is Element of the carrier of S
C is Element of the carrier of S
S . C is Element of the carrier of T
the mapping of S . C is Element of the carrier of T
z is Element of the carrier of T
T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T
X is non empty transitive directed eventually-filtered NetStr over T
Lim X is Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
inf X is Element of the carrier of T
{(inf X)} is non empty finite Element of K22( the carrier of T)
the mapping of X is Relation-like the carrier of X -defined the carrier of T -valued Function-like non empty V29( the carrier of X, the carrier of T) Element of K22(K23( the carrier of X, the carrier of T))
the carrier of X is non empty set
K23( the carrier of X, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of X, the carrier of T)) is non empty set
rng the mapping of X is non empty Element of K22( the carrier of T)
the topology of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T is non empty Element of K22(K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T))
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T is non empty set
K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T) is non empty set
K22(K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T)) is non empty set
sigma T is Element of K22(K22( the carrier of T))
K22(K22( the carrier of T)) is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T is Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T -valued Element of K22(K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T))
K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T) is Relation-like non empty set
K22(K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T #) is strict RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
//\ ( the mapping of X,T) is Element of the carrier of T
Y is non empty filtered Element of K22( the carrier of T)
"/\" (Y,T) is Element of the carrier of T
dom the mapping of X is non empty Element of K22( the carrier of X)
K22( the carrier of X) is non empty set
F is set
iN is Element of the carrier of T
jN is Element of the carrier of T
j is set
the mapping of X . j is set
Xj is Element of the carrier of X
X . Xj is Element of the carrier of T
the mapping of X . Xj is Element of the carrier of T
j is Element of the carrier of X
downarrow jN is non empty directed lower Element of K22( the carrier of T)
{jN} is non empty finite Element of K22( the carrier of T)
downarrow {jN} is non empty lower Element of K22( the carrier of T)
Cl (downarrow jN) is closed Element of K22( the carrier of T)
G is Element of the carrier of X
X . G is Element of the carrier of T
the mapping of X . G is Element of the carrier of T
uparrow (inf X) is non empty filtered upper Element of K22( the carrier of T)
uparrow {(inf X)} is non empty upper Element of K22( the carrier of T)
Cl (uparrow (inf X)) is closed Element of K22( the carrier of T)
Cl Y is closed Element of K22( the carrier of T)
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of T : verum } is set
(sigma T) \/ { ((uparrow b<sub>1</sub>) `) where b₁ is Element of the carrier of T : verum } is set
iN is Element of K22( the carrier of T)
F is quasi_prebasis V123(T) Element of K22(K22( the carrier of T))
jN is Element of K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T)
the Element of the carrier of X is Element of the carrier of X
Xj is Element of the carrier of X
X . Xj is Element of the carrier of T
the mapping of X . Xj is Element of the carrier of T
jN is Element of the carrier of T
uparrow jN is non empty filtered upper Element of K22( the carrier of T)
{jN} is non empty finite Element of K22( the carrier of T)
uparrow {jN} is non empty upper Element of K22( the carrier of T)
(uparrow jN) ` is lower Element of K22( the carrier of T)
j is Element of the carrier of T
Xj is set
the mapping of X . Xj is set
j is Element of the carrier of X
X . j is Element of the carrier of T
the mapping of X . j is Element of the carrier of T
G is Element of the carrier of X
C is Element of the carrier of X
X . C is Element of the carrier of T
the mapping of X . C is Element of the carrier of T
T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
S is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopRelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
K22( the carrier of T) is non empty set
[#] S is non empty non proper open closed dense non boundary directed filtered lower upper Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T
the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S is non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T
the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T is Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T -valued Element of K22(K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T))
K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T) is Relation-like non empty set
K22(K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T #) is strict RelStr
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T -valued Element of K22(K23( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T))
K23( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T) is Relation-like non empty set
K22(K23( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T #) is strict RelStr
the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S is non empty set
the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S is Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S -valued Element of K22(K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S))
K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S) is Relation-like non empty set
K22(K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S, the InternalRel of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S #) is strict RelStr
the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of K22(K23( the carrier of S, the carrier of S))
K23( the carrier of S, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of S, the carrier of S)) is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is strict RelStr
the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S is non empty set
the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S -valued Element of K22(K23( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S))
K23( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S) is Relation-like non empty set
K22(K23( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S, the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S #) is strict RelStr
jN is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone meet-preserving Element of K22(K23( the carrier of T, the carrier of S))
K23( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S) is Relation-like non empty set
K22(K23( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S)) is non empty set
K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S) is Relation-like non empty set
K22(K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S)) is non empty set
[#] the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S is non empty non proper open closed dense non boundary directed filtered lower upper Element of K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S)
K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S) is non empty set
j is Element of K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S)
G is Element of K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S)
C is Element of K22( the carrier of S)
jN " C is Element of K22( the carrier of T)
Xj is Relation-like the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T -defined the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S -valued Function-like V29( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S) Element of K22(K23( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T, the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of S))
Xj " G is Element of K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T)
K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T) is non empty set
Xj " j is Element of K22( the carrier of the non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Scott TopAugmentation of T)
j is non empty filtered Element of K22( the carrier of T)
jN .: j is non empty Element of K22( the carrier of S)
"/\" ((jN .: j),S) is Element of the carrier of S
"/\" (j,T) is Element of the carrier of T
jN . ("/\" (j,T)) is Element of the carrier of S
{("/\" (j,T))} is non empty finite Element of K22( the carrier of T)
j opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over T
Lim (j opp+id) is Element of K22( the carrier of T)
Im (jN,("/\" (j,T))) is set
{("/\" (j,T))} is non empty finite set
jN .: {("/\" (j,T))} is finite set
jN * (j opp+id) is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over S
Lim (jN * (j opp+id)) is Element of K22( the carrier of S)
jN . ("/\" (j,T)) is Element of the carrier of S
{(jN . ("/\" (j,T)))} is non empty finite Element of K22( the carrier of S)
the mapping of (jN * (j opp+id)) is Relation-like the carrier of (jN * (j opp+id)) -defined the carrier of S -valued Function-like non empty V29( the carrier of (jN * (j opp+id)), the carrier of S) Element of K22(K23( the carrier of (jN * (j opp+id)), the carrier of S))
the carrier of (jN * (j opp+id)) is non empty set
K23( the carrier of (jN * (j opp+id)), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (jN * (j opp+id)), the carrier of S)) is non empty set
rng the mapping of (jN * (j opp+id)) is non empty Element of K22( the carrier of S)
the carrier of (j opp+id) is non empty set
the mapping of (j opp+id) is Relation-like the carrier of (j opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of (j opp+id), the carrier of T) Element of K22(K23( the carrier of (j opp+id), the carrier of T))
K23( the carrier of (j opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (j opp+id), the carrier of T)) is non empty set
jN * the mapping of (j opp+id) is Relation-like the carrier of (j opp+id) -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of (j opp+id), the carrier of S))
K23( the carrier of (j opp+id), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (j opp+id), the carrier of S)) is non empty set
rng (jN * the mapping of (j opp+id)) is Element of K22( the carrier of S)
id j is Relation-like j -defined j -valued Function-like one-to-one non empty V24(j) Element of K22(K23(j,j))
K23(j,j) is Relation-like non empty set
K22(K23(j,j)) is non empty set
jN * (id j) is Relation-like j -defined the carrier of S -valued Function-like Element of K22(K23(j, the carrier of S))
K23(j, the carrier of S) is Relation-like non empty set
K22(K23(j, the carrier of S)) is non empty set
rng (jN * (id j)) is Element of K22( the carrier of S)
jN | j is Relation-like the carrier of T -defined j -defined the carrier of T -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of T, the carrier of S))
rng (jN | j) is Element of K22( the carrier of S)
G is non empty filtered Element of K22( the carrier of S)
inf (jN * (j opp+id)) is Element of the carrier of S
{(inf (jN * (j opp+id)))} is non empty finite Element of K22( the carrier of S)
//\ ( the mapping of (jN * (j opp+id)),S) is Element of the carrier of S
{(//\ ( the mapping of (jN * (j opp+id)),S))} is non empty finite Element of K22( the carrier of S)
"/\" (G,S) is Element of the carrier of S
{("/\" (G,S))} is non empty finite Element of K22( the carrier of S)
j is non empty Element of K22( the carrier of T)
K22( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T) is non empty set
j is Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S -valued Function-like V29( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S) Element of K22(K23( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T, the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of S))
j is non empty Element of K22( the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete lower TopAugmentation of T)
T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
S is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopRelStr
the carrier of S is non empty set
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone meet-preserving (T,S)
K22( the carrier of T) is non empty set
Y is finite Element of K22( the carrier of T)
Y is non empty filtered Element of K22( the carrier of T)
Y is non empty Element of K22( the carrier of T)
T is non empty RelStr
the carrier of T is non empty set
S is non empty RelStr
the carrier of S is non empty set
K23( the carrier of T, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of S)) is non empty set
T is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
S is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopRelStr
the carrier of S is non empty set
X is Relation-like the carrier of T -defined the carrier of S -valued Function-like V29( the carrier of T, the carrier of S) monotone meet-preserving (T,S)
Y is non empty transitive directed NetStr over T
lim_inf Y is Element of the carrier of T
X . (lim_inf Y) is Element of the carrier of S
X * Y is non empty transitive strict directed NetStr over S
lim_inf (X * Y) is Element of the carrier of S
the carrier of (X * Y) is non empty set
{ ("/\" ( { ((X * Y) . b₂) where b₂ is Element of the carrier of (X * Y) : b₁ <= b₂ } ,S)) where b₁ is Element of the carrier of (X * Y) : verum } is set
K22( the carrier of T) is non empty set
the carrier of Y is non empty set
{ ("/\" ( { (Y . b₂) where b₂ is Element of the carrier of Y : b₁ <= b₂ } ,T)) where b₁ is Element of the carrier of Y : verum } is set
jN is non empty directed Element of K22( the carrier of T)
the InternalRel of (X * Y) is Relation-like the carrier of (X * Y) -defined the carrier of (X * Y) -valued Element of K22(K23( the carrier of (X * Y), the carrier of (X * Y)))
K23( the carrier of (X * Y), the carrier of (X * Y)) is Relation-like non empty set
K22(K23( the carrier of (X * Y), the carrier of (X * Y))) is non empty set
RelStr(# the carrier of (X * Y), the InternalRel of (X * Y) #) is strict RelStr
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr
dom X is Element of K22( the carrier of T)
{ (Y . b₁) where b₁ is Element of the carrier of Y : a₁ <= b₁ } is set
{ H₂(b₁) where b₁ is Element of the carrier of Y : S₁[b₁] } is set
X .: { H₂(b₁) where b₁ is Element of the carrier of Y : S₁[b₁] } is Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
{ (X . H₂(b₁)) where b₁ is Element of the carrier of Y : S₁[b₁] } is set
X .: jN is non empty Element of K22( the carrier of S)
Xj is Element of the carrier of (X * Y)
j is Element of the carrier of Y
the mapping of Y is Relation-like the carrier of Y -defined the carrier of T -valued Function-like non empty V29( the carrier of Y, the carrier of T) Element of K22(K23( the carrier of Y, the carrier of T))
K23( the carrier of Y, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of T)) is non empty set
j is Element of the carrier of Y
Y . j is Element of the carrier of T
the mapping of Y . j is Element of the carrier of T
X . (Y . j) is Element of the carrier of S
the mapping of Y . j is set
X . ( the mapping of Y . j) is set
X * the mapping of Y is Relation-like the carrier of Y -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of Y, the carrier of S))
K23( the carrier of Y, the carrier of S) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of S)) is non empty set
j is Element of the carrier of Y
the mapping of Y . j is set
X . ( the mapping of Y . j) is set
(X * the mapping of Y) . j is set
j is Element of the carrier of (X * Y)
(X * the mapping of Y) . j is set
(X * Y) . j is Element of the carrier of S
the mapping of (X * Y) is Relation-like the carrier of (X * Y) -defined the carrier of S -valued Function-like non empty V29( the carrier of (X * Y), the carrier of S) Element of K22(K23( the carrier of (X * Y), the carrier of S))
K23( the carrier of (X * Y), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (X * Y), the carrier of S)) is non empty set
the mapping of (X * Y) . j is Element of the carrier of S
j is Element of the carrier of Y
[Xj,j] is set
{Xj,j} is non empty finite set
{Xj} is non empty finite set
{{Xj,j},{Xj}} is non empty finite V43() set
G is Element of the carrier of Y
[Xj,G] is set
{Xj,G} is non empty finite set
{{Xj,G},{Xj}} is non empty finite V43() set
j is Element of the carrier of (X * Y)
[Xj,j] is set
{Xj,j} is non empty finite set
{Xj} is non empty finite set
{{Xj,j},{Xj}} is non empty finite V43() set
G is Element of the carrier of (X * Y)
[Xj,G] is set
{Xj,G} is non empty finite set
{{Xj,G},{Xj}} is non empty finite V43() set
{ (Y . b₁) where b₁ is Element of the carrier of Y : j <= b₁ } is set
X .: H₁(j) is Element of K22( the carrier of S)
{ H₇(b₁) where b₁ is Element of the carrier of Y : S₂[b₁] } is set
X .: { H₇(b₁) where b₁ is Element of the carrier of Y : S₂[b₁] } is Element of K22( the carrier of S)
{ (X . H₇(b₁)) where b₁ is Element of the carrier of Y : S₂[b₁] } is set
{ H₃(b₁) where b₁ is Element of the carrier of Y : S₂[b₁] } is set
{ H₄(b₁) where b₁ is Element of the carrier of Y : S₂[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Y : S₂[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of Y : S₄[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of (X * Y) : S₄[b₁] } is set
{ H₅(b₁) where b₁ is Element of the carrier of (X * Y) : S₃[b₁] } is set
{ H₆(b₁) where b₁ is Element of the carrier of (X * Y) : S₃[b₁] } is set
{ ((X * Y) . b₁) where b₁ is Element of the carrier of (X * Y) : Xj <= b₁ } is set
j is Element of the carrier of Y
{ (Y . b₁) where b₁ is Element of the carrier of Y : j <= b₁ } is set
Xj is set
j is Element of the carrier of Y
Y . j is Element of the carrier of T
the mapping of Y . j is Element of the carrier of T
Xj is Element of K22( the carrier of T)
"/\" (H₁(j),T) is Element of the carrier of T
X . ("/\" (H₁(j),T)) is Element of the carrier of S
X .: H₁(j) is Element of K22( the carrier of S)
"/\" ((X .: H₁(j)),S) is Element of the carrier of S
j is set
Xj is Element of the carrier of Y
{ (Y . b₁) where b₁ is Element of the carrier of Y : Xj <= b₁ } is set
"/\" ( { (Y . b₁) where b₁ is Element of the carrier of Y : Xj <= b₁ } ,T) is Element of the carrier of T
X . ("/\" ( { (Y . b₁) where b₁ is Element of the carrier of Y : Xj <= b₁ } ,T)) is Element of the carrier of S
X .: H₁(Xj) is Element of K22( the carrier of S)
"/\" ((X .: H₁(Xj)),S) is Element of the carrier of S
j is Element of the carrier of (X * Y)
{ ((X * Y) . b₁) where b₁ is Element of the carrier of (X * Y) : j <= b₁ } is set
j is set
Xj is Element of the carrier of (X * Y)
{ ((X * Y) . b₁) where b₁ is Element of the carrier of (X * Y) : Xj <= b₁ } is set
"/\" ( { ((X * Y) . b₁) where b₁ is Element of the carrier of (X * Y) : Xj <= b₁ } ,S) is Element of the carrier of S
j is Element of the carrier of Y
{ (Y . b₁) where b₁ is Element of the carrier of Y : j <= b₁ } is set
X .: H₁(j) is Element of K22( the carrier of S)
"/\" ((X .: H₁(j)),S) is Element of the carrier of S
"/\" (H₁(j),T) is Element of the carrier of T
X . ("/\" (H₁(j),T)) is Element of the carrier of S
"\/" (jN,T) is Element of the carrier of T
X . ("\/" (jN,T)) is Element of the carrier of S
"\/" ((X .: jN),S) is Element of the carrier of S
K22( the carrier of T) is non empty set
Y is Element of K22( the carrier of T)
X .: Y is Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
"\/" ((X .: Y),S) is Element of the carrier of S
"\/" (Y,T) is Element of the carrier of T
X . ("\/" (Y,T)) is Element of the carrier of S
X . ("\/" (Y,T)) is Element of the carrier of S
F is non empty directed Element of K22( the carrier of T)
Net-Str F is non empty reflexive transitive strict directed monotone eventually-directed NetStr over T
lim_inf (Net-Str F) is Element of the carrier of T
X . (lim_inf (Net-Str F)) is Element of the carrier of S
X * (Net-Str F) is non empty reflexive transitive strict directed monotone eventually-directed NetStr over S
lim_inf (X * (Net-Str F)) is Element of the carrier of S
K22( the carrier of T) is non empty set
Y is finite Element of K22( the carrier of T)
K22( the carrier of S) is non empty set
Y is non empty filtered Element of K22( the carrier of T)
X .: Y is non empty Element of K22( the carrier of S)
"/\" ((X .: Y),S) is Element of the carrier of S
"/\" (Y,T) is Element of the carrier of T
X . ("/\" (Y,T)) is Element of the carrier of S
X . ("/\" (Y,T)) is Element of the carrier of S
Y opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over T
lim_inf (Y opp+id) is Element of the carrier of T
X . (lim_inf (Y opp+id)) is Element of the carrier of S
X * (Y opp+id) is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over S
lim_inf (X * (Y opp+id)) is Element of the carrier of S
F is non empty filtered Element of K22( the carrier of S)
"/\" (F,S) is Element of the carrier of S
F opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over S
lim_inf (F opp+id) is Element of the carrier of S
T is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete continuous with_suprema with_infima complete Lawson compact TopRelStr
Top T is Element of the carrier of T
the carrier of T is non empty set
"/\" ({},T) is Element of the carrier of T
K22( the carrier of T) is non empty set
S is non empty reflexive transitive antisymmetric full meet-inheriting with_infima SubRelStr of T
the carrier of S is non empty set
X is Element of K22( the carrier of T)
K22( the carrier of S) is non empty set
Y is filtered Element of K22( the carrier of S)
"/\" (Y,T) is Element of the carrier of T
F is non empty filtered Element of K22( the carrier of T)
F opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over T
the mapping of (F opp+id) is Relation-like the carrier of (F opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of (F opp+id), the carrier of T) Element of K22(K23( the carrier of (F opp+id), the carrier of T))
the carrier of (F opp+id) is non empty set
K23( the carrier of (F opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (F opp+id), the carrier of T)) is non empty set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one V24(Y) Element of K22(K23(Y,Y))
K23(Y,Y) is Relation-like set
K22(K23(Y,Y)) is non empty set
rng the mapping of (F opp+id) is non empty Element of K22( the carrier of T)
Lim (F opp+id) is V14() finite Element of K22( the carrier of T)
"/\" (F,T) is Element of the carrier of T
{("/\" (F,T))} is non empty finite Element of K22( the carrier of T)
Cl X is closed Element of K22( the carrier of T)
T is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete continuous with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty reflexive transitive antisymmetric full SubRelStr of T
the carrier of S is non empty set
X is Element of K22( the carrier of T)
K22( the carrier of S) is non empty set
Y is directed Element of K22( the carrier of S)
"\/" (Y,T) is Element of the carrier of T
F is non empty directed Element of K22( the carrier of T)
Net-Str F is non empty reflexive transitive strict directed monotone eventually-directed NetStr over T
the mapping of (Net-Str F) is Relation-like the carrier of (Net-Str F) -defined the carrier of T -valued Function-like non empty V29( the carrier of (Net-Str F), the carrier of T) Element of K22(K23( the carrier of (Net-Str F), the carrier of T))
the carrier of (Net-Str F) is non empty set
K23( the carrier of (Net-Str F), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (Net-Str F), the carrier of T)) is non empty set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one V24(Y) Element of K22(K23(Y,Y))
K23(Y,Y) is Relation-like set
K22(K23(Y,Y)) is non empty set
rng the mapping of (Net-Str F) is non empty Element of K22( the carrier of T)
Lim (Net-Str F) is V14() finite Element of K22( the carrier of T)
Cl X is closed Element of K22( the carrier of T)
"\/" (F,T) is Element of the carrier of T
T is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete continuous with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
S is non empty reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting with_infima SubRelStr of T
the carrier of S is non empty set
X is Element of K22( the carrier of T)
Y is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V164() full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting up-complete /\-complete with_suprema with_infima complete SubRelStr of T
the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y is non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y
the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y is non empty set
the InternalRel of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y is Relation-like the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y -defined the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y -valued Element of K22(K23( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y, the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y))
K23( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y, the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y) is Relation-like non empty set
K22(K23( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y, the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y)) is non empty set
RelStr(# the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y, the InternalRel of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y #) is strict RelStr
the carrier of Y is non empty set
the InternalRel of Y is Relation-like the carrier of Y -defined the carrier of Y -valued Element of K22(K23( the carrier of Y, the carrier of Y))
K23( the carrier of Y, the carrier of Y) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of Y)) is non empty set
RelStr(# the carrier of Y, the InternalRel of Y #) is strict RelStr
incl ( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y,T) is Relation-like the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y -defined the carrier of T -valued Function-like V29( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y, the carrier of T) Element of K22(K23( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y, the carrier of T))
K23( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y, the carrier of T)) is non empty set
incl (Y,T) is Relation-like the carrier of Y -defined the carrier of T -valued Function-like V29( the carrier of Y, the carrier of T) monotone Element of K22(K23( the carrier of Y, the carrier of T))
K23( the carrier of Y, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of T)) is non empty set
id the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y is Relation-like the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y -defined the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y -valued Function-like one-to-one non empty V24( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y) Element of K22(K23( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y, the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y))
[#] the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y is non empty non proper open closed dense non boundary directed filtered lower upper Element of K22( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y)
K22( the carrier of the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y) is non empty set
the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of K22(K23( the carrier of T, the carrier of T))
K23( the carrier of T, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of T, the carrier of T)) is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr
(incl ( the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y,T)) .: ([#] the non empty TopSpace-like T_0 T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete with_suprema with_infima complete Lawson compact TopAugmentation of Y) is non empty Element of K22( the carrier of T)
T is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete continuous with_suprema with_infima complete Lawson compact TopRelStr
S is non empty reflexive transitive antisymmetric full meet-inheriting infs-inheriting filtered-infs-inheriting directed-sups-inheriting with_infima SubRelStr of T
the carrier of S is non empty set
Y is non empty transitive directed NetStr over T
lim_inf Y is Element of the carrier of T
the carrier of T is non empty set
the carrier of Y is non empty set
F is Element of the carrier of Y
Y . F is Element of the carrier of T
the mapping of Y is Relation-like the carrier of Y -defined the carrier of T -valued Function-like non empty V29( the carrier of Y, the carrier of T) Element of K22(K23( the carrier of Y, the carrier of T))
K23( the carrier of Y, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of T)) is non empty set
the mapping of Y . F is Element of the carrier of T
Y | F is non empty transitive strict directed subnet of Y
the mapping of (Y | F) is Relation-like the carrier of (Y | F) -defined the carrier of T -valued Function-like non empty V29( the carrier of (Y | F), the carrier of T) Element of K22(K23( the carrier of (Y | F), the carrier of T))
the carrier of (Y | F) is non empty set
K23( the carrier of (Y | F), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (Y | F), the carrier of T)) is non empty set
rng the mapping of (Y | F) is non empty Element of K22( the carrier of T)
K22( the carrier of T) is non empty set
{ ((Y | F) . b₁) where b₁ is Element of the carrier of (Y | F) : a₁ <= b₁ } is set
{ ("/\" (H₁(b₁),T)) where b₁ is Element of the carrier of (Y | F) : verum } is set
iN is non empty directed Element of K22( the carrier of T)
jN is set
j is Element of the carrier of (Y | F)
{ ((Y | F) . b₁) where b₁ is Element of the carrier of (Y | F) : j <= b₁ } is set
"/\" (H₁(j),T) is Element of the carrier of T
Xj is set
j is Element of the carrier of (Y | F)
(Y | F) . j is Element of the carrier of T
the mapping of (Y | F) . j is Element of the carrier of T
K22( the carrier of S) is non empty set
Xj is Element of K22( the carrier of S)
K22( the carrier of S) is non empty set
jN is non empty Element of K22( the carrier of S)
"\/" (jN,T) is Element of the carrier of T
lim_inf (Y | F) is Element of the carrier of T
T is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete continuous with_suprema with_infima complete Lawson compact TopRelStr
Top T is Element of the carrier of T
the carrier of T is non empty set
"/\" ({},T) is Element of the carrier of T
S is non empty reflexive transitive antisymmetric full meet-inheriting with_infima SubRelStr of T
the carrier of S is non empty set
K22( the carrier of S) is non empty set
Y is filtered Element of K22( the carrier of S)
"/\" (Y,T) is Element of the carrier of T
K22( the carrier of T) is non empty set
F is non empty filtered Element of K22( the carrier of T)
F opp+id is non empty reflexive transitive strict directed antitone eventually-filtered NetStr over T
the mapping of (F opp+id) is Relation-like the carrier of (F opp+id) -defined the carrier of T -valued Function-like non empty V29( the carrier of (F opp+id), the carrier of T) Element of K22(K23( the carrier of (F opp+id), the carrier of T))
the carrier of (F opp+id) is non empty set
K23( the carrier of (F opp+id), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (F opp+id), the carrier of T)) is non empty set
id F is Relation-like F -defined F -valued Function-like one-to-one non empty V24(F) Element of K22(K23(F,F))
K23(F,F) is Relation-like non empty set
K22(K23(F,F)) is non empty set
rng the mapping of (F opp+id) is non empty Element of K22( the carrier of T)
lim_inf (F opp+id) is Element of the carrier of T
"/\" (F,T) is Element of the carrier of T
T is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete continuous with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric full SubRelStr of T
the carrier of S is non empty set
K22( the carrier of S) is non empty set
Y is directed Element of K22( the carrier of S)
"\/" (Y,T) is Element of the carrier of T
K22( the carrier of T) is non empty set
F is non empty directed Element of K22( the carrier of T)
Net-Str F is non empty reflexive transitive strict directed monotone eventually-directed NetStr over T
the mapping of (Net-Str F) is Relation-like the carrier of (Net-Str F) -defined the carrier of T -valued Function-like non empty V29( the carrier of (Net-Str F), the carrier of T) Element of K22(K23( the carrier of (Net-Str F), the carrier of T))
the carrier of (Net-Str F) is non empty set
K23( the carrier of (Net-Str F), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (Net-Str F), the carrier of T)) is non empty set
id F is Relation-like F -defined F -valued Function-like one-to-one non empty V24(F) Element of K22(K23(F,F))
K23(F,F) is Relation-like non empty set
K22(K23(F,F)) is non empty set
rng the mapping of (Net-Str F) is non empty Element of K22( the carrier of T)
lim_inf (Net-Str F) is Element of the carrier of T
"\/" (F,T) is Element of the carrier of T
T is non empty TopSpace-like T_0 T_1 T_2 reflexive transitive antisymmetric lower-bounded upper-bounded V164() up-complete /\-complete continuous with_suprema with_infima complete Lawson compact TopRelStr
the carrier of T is non empty set
K22( the carrier of T) is non empty set
Top T is Element of the carrier of T
"/\" ({},T) is Element of the carrier of T
S is non empty reflexive transitive antisymmetric full meet-inheriting with_infima SubRelStr of T
the carrier of S is non empty set
X is Element of K22( the carrier of T)
Y is non empty transitive directed NetStr over T
lim_inf Y is Element of the carrier of T
Y is non empty transitive directed NetStr over T
the mapping of Y is Relation-like the carrier of Y -defined the carrier of T -valued Function-like non empty V29( the carrier of Y, the carrier of T) Element of K22(K23( the carrier of Y, the carrier of T))
the carrier of Y is non empty set
K23( the carrier of Y, the carrier of T) is Relation-like non empty set
K22(K23( the carrier of Y, the carrier of T)) is non empty set
rng the mapping of Y is non empty Element of K22( the carrier of T)
lim_inf Y is Element of the carrier of T
Y is Element of K22( the carrier of T)