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

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

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

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

the carrier of T is non empty set

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

the carrier of T is non empty set

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

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

K22( the carrier of S) is non empty set
"/\" ((X .: ({} T)),S) is Element of the carrier of S

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
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 .: {}),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

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

K22( the carrier of S) is non empty set

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

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

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

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

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

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

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

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

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

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

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

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
{ ("\/" (b1,T)) where b1 is finite Element of K22(Y) : ex_sup_of b1,T } is set
"\/" ((),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)

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

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 () is non empty set
Y is Element of the carrier of ()
F is Element of the carrier of ()
iN is Element of the carrier of ()
Y is Element of the carrier of ()
F is Element of the carrier of ()
Y is Element of the carrier of ()
F is Element of the carrier of ()
netmap ((),T) is Relation-like the carrier of () -defined the carrier of T -valued Function-like V29( the carrier of (), the carrier of T) Element of K22(K23( the carrier of (), the carrier of T))
K23( the carrier of (), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of T)) is non empty set
the mapping of () is Relation-like the carrier of () -defined the carrier of T -valued Function-like non empty V29( the carrier of (), the carrier of T) Element of K22(K23( the carrier of (), the carrier of T))
(netmap ((),T)) . Y is Element of the carrier of T
(netmap ((),T)) . F is Element of the carrier of T
Y is Element of the carrier of ()
F is Element of the carrier of ()
() . F is Element of the carrier of T
the mapping of () is Relation-like the carrier of () -defined the carrier of T -valued Function-like non empty V29( the carrier of (), the carrier of T) Element of K22(K23( the carrier of (), the carrier of T))
K23( the carrier of (), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of T)) is non empty set
the mapping of () . F is Element of the carrier of T
() . Y is Element of the carrier of T
the mapping of () . 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 () is non empty set
X is Element of the carrier of ()
Y is Element of the carrier of ()
() . Y is Element of the carrier of T
the mapping of () is Relation-like the carrier of () -defined the carrier of T -valued Function-like non empty V29( the carrier of (), the carrier of T) Element of K22(K23( the carrier of (), the carrier of T))
K23( the carrier of (), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of T)) is non empty set
the mapping of () . Y is Element of the carrier of T
() . X is Element of the carrier of T
the mapping of () . 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

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 . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 is Element of the carrier of S : verum } is set
Y is set
F is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : F <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : F <= b1 } ,T) is Element of the carrier of T
Y is Element of K22( the carrier of T)

the carrier of T is non empty set
K22( the carrier of T) is non empty set

the carrier of S is non empty set
{ ("/\" ( { (S . b2) where b2 is Element of the carrier of S : b1 <= b2 } ,T)) where b1 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 . b1) where b1 is Element of the carrier of S : the Element of the carrier of S <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : the Element of the carrier of S <= b1 } ,T) is Element of the carrier of T
F is set
iN is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : iN <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : iN <= b1 } ,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 . b1) where b1 is Element of the carrier of S : j <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : j <= b1 } ,T) is Element of the carrier of T
Xj is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : Xj <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : Xj <= b1 } ,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 . b1) where b1 is Element of the carrier of S : C <= b1 } is set
"/\" ( { (S . b1) where b1 is Element of the carrier of S : C <= b1 } ,T) is Element of the carrier of T
{ (S . b1) where b1 is Element of the carrier of S : a1 <= b1 } is set
k is Element of the carrier of S
{ (S . b1) where b1 is Element of the carrier of S : k <= b1 } 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
c18 is Element of the carrier of S
S . c18 is Element of the carrier of T
the mapping of S . c18 is Element of the carrier of T
k is Element of the carrier of T
k is Element of the carrier of T
{ (S . b1) where b1 is Element of the carrier of S : j <= b1 } is set
{ (S . b1) where b1 is Element of the carrier of S : G <= b1 } 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

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)

lim_inf () is Element of the carrier of T
"/\" (S,T) is Element of the carrier of T
the carrier of () is non empty set
{ (() . b1) where b1 is Element of the carrier of () : a1 <= b1 } is set
"/\" ( { (() . b1) where b1 is Element of the carrier of () : a1 <= b1 } ,T) is Element of the carrier of T
Y is Element of the carrier of ()
{ (() . b1) where b1 is Element of the carrier of () : Y <= b1 } is set
"/\" ( { (() . b1) where b1 is Element of the carrier of () : Y <= b1 } ,T) is Element of the carrier of T
j is set
Xj is Element of the carrier of ()
() . Xj is Element of the carrier of T
the mapping of () is Relation-like the carrier of () -defined the carrier of T -valued Function-like non empty V29( the carrier of (), the carrier of T) Element of K22(K23( the carrier of (), the carrier of T))
K23( the carrier of (), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of T)) is non empty set
the mapping of () . Xj is Element of the carrier of T
j is Element of the carrier of ()
jN is Element of the carrier of ()
() . Y is Element of the carrier of T
the mapping of () is Relation-like the carrier of () -defined the carrier of T -valued Function-like non empty V29( the carrier of (), the carrier of T) Element of K22(K23( the carrier of (), the carrier of T))
K23( the carrier of (), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of T)) is non empty set
the mapping of () . 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

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 ()
() . G is Element of the carrier of T
the mapping of () . 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
{ H1(b1) where b1 is Element of the carrier of () : S1[b1] } is set
{ H2(b1) where b1 is Element of the carrier of () : S1[b1] } is set
{ ("/\" (S,T)) where b1 is Element of the carrier of () : S1[b1] } 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

the carrier of T is non empty set
K22( 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
X is non empty filtered Element of K22( the carrier of 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))

lim_inf (Y * ()) 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 * ()) is non empty set
{ ((Y * ()) . b1) where b1 is Element of the carrier of (Y * ()) : a1 <= b1 } 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 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 carrier of () is non empty set
the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued Element of K22(K23( the carrier of (), the carrier of ()))
K23( the carrier of (), the carrier of ()) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of ())) is non empty set
RelStr(# the carrier of (), the InternalRel of () #) is strict RelStr
the mapping of (Y * ()) is Relation-like the carrier of (Y * ()) -defined the carrier of S -valued Function-like non empty 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
the mapping of () is Relation-like the carrier of () -defined the carrier of T -valued Function-like non empty V29( the carrier of (), the carrier of T) Element of K22(K23( the carrier of (), the carrier of T))
K23( the carrier of (), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of T)) is non empty set
Y * the mapping of () is Relation-like the carrier of () -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of (), the carrier of S))
K23( the carrier of (), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (), 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 * ())
{ ((Y * ()) . b1) where b1 is Element of the carrier of (Y * ()) : jN <= b1 } is set
"/\" (H1(jN),S) is Element of the carrier of S
[#] (Y * ()) is non empty non proper lower upper Element of K22( the carrier of (Y * ()))
K22( the carrier of (Y * ())) is non empty set
j is Element of the carrier of (Y * ())
Xj is Element of the carrier of (Y * ())
{ ((Y * ()) . b1) where b1 is Element of the carrier of (Y * ()) : j <= b1 } is set
j is set
G is Element of the carrier of (Y * ())
(Y * ()) . G is Element of the carrier of S
the mapping of (Y * ()) . G is Element of the carrier of S
C is Element of the carrier of (Y * ())
(Y * ()) . C is Element of the carrier of S
the mapping of (Y * ()) . 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 ()
Y . z is set
(Y * ()) . Xj is Element of the carrier of S
the mapping of (Y * ()) . Xj is Element of the carrier of S
"/\" (H1(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 * ())
z is Element of the carrier of (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
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 * ()) . z is Element of the carrier of S
the mapping of (Y * ()) . z is Element of the carrier of S
(id X) . z is set
Y . ((id X) . z) is set
{ H2(b1) where b1 is Element of the carrier of (Y * ()) : S1[b1] } is set
{ H3(b1) where b1 is Element of the carrier of (Y * ()) : S1[b1] } is set
{ ("/\" ((Y .: X),S)) where b1 is Element of the carrier of (Y * ()) : S1[b1] } 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

the carrier of T is non empty set
K22( 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 S) is non empty set
X is non empty filtered Element of K22( the carrier of 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)

F is non empty filtered Element of K22( the carrier 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 carrier of () is non empty set
the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued Element of K22(K23( the carrier of (), the carrier of ()))
K23( the carrier of (), the carrier of ()) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of ())) is non empty set
RelStr(# the carrier of (), the InternalRel of () #) is strict RelStr
the mapping of (Y * ()) is Relation-like the carrier of (Y * ()) -defined the carrier of S -valued Function-like non empty 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
the mapping of () is Relation-like the carrier of () -defined the carrier of T -valued Function-like non empty V29( the carrier of (), the carrier of T) Element of K22(K23( the carrier of (), the carrier of T))
K23( the carrier of (), the carrier of T) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of T)) is non empty set
Y * the mapping of () is Relation-like the carrier of () -defined the carrier of S -valued Function-like Element of K22(K23( the carrier of (), the carrier of S))
K23( the carrier of (), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (), the carrier of S)) is non empty set
the carrier of () is non empty set
the mapping of () is Relation-like the carrier of () -defined the carrier of S -valued Function-like non empty V29( the carrier of (), the carrier of S) Element of K22(K23( the carrier of (), the carrier of S))
K23( the carrier of (), the carrier of S) is Relation-like non empty set
K22(K23( the carrier of (), 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 * ()) is non empty Element of K22( the carrier of S)
dom the mapping of (Y * ()) is non empty Element of K22( the carrier of (Y * ()))
K22( the carrier of (Y * ())) is non empty set
K23( the carrier of (Y * ()), the carrier of ()) is Relation-like non empty set
K22(K23( the carrier of (Y * ()), the carrier of ())) is non empty set
j is Relation-like the carrier of (Y * ()) -defined the carrier of () -valued Function-like V29( the carrier of (Y * ()), the carrier of ()) Element of K22(K23( the carrier of (Y * ()), the carrier of ()))
the mapping of () * j 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))
Xj is Element of the carrier of ()
j is set
Y . j is set
G is Element of the carrier of (Y * ())
C is Element of the carrier of (Y * ())
j . C is Element of the carrier of ()
k is Element of the carrier of T
Y . k is Element of the carrier of S

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

the carrier of T is non empty set
K22( 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 S) is non empty set
X is non empty filtered Element of K22( the carrier of 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)

Lim (Y * ()) is Element of K22( the carrier of S)
F is non empty filtered Element of K22( the carrier of S)

Lim () 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 () is Relation-like the carrier of () -defined the carrier of T -valued Function-like V29( the carrier of (), the carrier of T) Element of K22(K23( the carrier of (), the carrier of T))
the carrier of () is set
K23( the carrier of (), the carrier of T) is Relation-like set
K22(K23( the carrier of (), 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 () is Relation-like the carrier of () -defined the carrier of () -valued Element of K22(K23( the carrier of (), the carrier of ()))
K23( the carrier of (), the carrier of ()) is Relation-like set
K22(K23( the carrier of (), the carrier of ())) is non empty set

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

X * () is non empty reflexive transitive strict directed NetStr over S
lim_inf (X * ()) 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