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