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

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

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

Y is set

F is Element of the carrier of S

{ (S . b

"/\" ( { (S . b

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

the Element of the carrier of S is Element of the carrier of S

{ (S . b

"/\" ( { (S . b

F is set

iN is Element of the carrier of S

{ (S . b

"/\" ( { (S . b

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

"/\" ( { (S . b

Xj is Element of the carrier of S

{ (S . b

"/\" ( { (S . b

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

"/\" ( { (S . b

{ (S . b

k is Element of the carrier of S

{ (S . b

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

S . c

the mapping of S . c

k is Element of the carrier of T

k is Element of the carrier of T

{ (S . b

{ (S . b

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

"/\" ( { ((S opp+id) . b

Y is Element of the carrier of (S opp+id)

{ ((S opp+id) . b

"/\" ( { ((S opp+id) . b

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

{ H

{ ("/\" (S,T)) where b

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

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

"/\" (H

[#] (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

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

{ H

{ ("/\" ((Y .: X),S)) where b

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