:: POSET_1 semantic presentation

K136() is set
K140() is non empty V24() V25() V26() Element of K19(K136())
K19(K136()) is set
K88() is non empty V24() V25() V26() set
K19(K88()) is set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V94() V117() ext-real non negative V121() set
1 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() Element of K140()
{{},1} is non empty set
K19(K140()) is set
0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V94() V117() ext-real non negative V121() Element of K140()
P is Relation-like Function-like set
rng P is set
dom P is set
iter (P,0) is Relation-like Function-like set
id (dom P) is Relation-like dom P -defined dom P -valued Function-like one-to-one V14( dom P) reflexive symmetric antisymmetric transitive Element of K19(K20((dom P),(dom P)))
K20((dom P),(dom P)) is Relation-like set
K19(K20((dom P),(dom P))) is set
field P is set
(dom P) \/ (rng P) is set
P is Relation-like Function-like set
rng P is set
dom P is set
f is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (P,f) is Relation-like Function-like set
dom (iter (P,f)) is set
rng (iter (P,f)) is set
iter (P,0) is Relation-like Function-like set
id (dom P) is Relation-like dom P -defined dom P -valued Function-like one-to-one V14( dom P) reflexive symmetric antisymmetric transitive Element of K19(K20((dom P),(dom P)))
K20((dom P),(dom P)) is Relation-like set
K19(K20((dom P),(dom P))) is set
dom (iter (P,0)) is set
rng (iter (P,0)) is set
h is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (P,h) is Relation-like Function-like set
dom (iter (P,h)) is set
rng (iter (P,h)) is set
h + 1 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (P,(h + 1)) is Relation-like Function-like set
dom (iter (P,(h + 1))) is set
rng (iter (P,(h + 1))) is set
(iter (P,h)) * P is Relation-like Function-like set
P * (iter (P,h)) is Relation-like Function-like set
P is set
K20(P,P) is Relation-like set
K19(K20(P,P)) is set
f is Relation-like P -defined P -valued Function-like quasi_total Element of K19(K20(P,P))
h is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,h) is Relation-like Function-like set
dom f is Element of K19(P)
K19(P) is set
rng f is Element of K19(P)
dom (iter (f,h)) is set
rng (iter (f,h)) is set
L is Relation-like P -defined P -valued Element of K19(K20(P,P))
dom L is Element of K19(P)
rng L is Element of K19(P)
P is non empty V55() reflexive transitive antisymmetric RelStr
the carrier of P is non empty set
K19( the carrier of P) is set
the Element of the carrier of P is Element of the carrier of P
{ the Element of the carrier of P} is non empty set
L is strongly_connected Element of K19( the carrier of P)
f is strongly_connected Element of K19( the carrier of P)
P is non empty RelStr
the carrier of P is non empty set
f is Element of the carrier of P
h is Element of the carrier of P
h is Element of the carrier of P
L is Element of the carrier of P
P is non empty V55() reflexive transitive antisymmetric RelStr
the carrier of P is non empty set
K19( the carrier of P) is set
f is non empty V55() reflexive transitive antisymmetric RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
K19( the carrier of f) is set
h is non empty strongly_connected Element of K19( the carrier of P)
L is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
L .: h is Element of K19( the carrier of f)
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued V14( the carrier of f) reflexive antisymmetric transitive Element of K19(K20( the carrier of f, the carrier of f))
K20( the carrier of f, the carrier of f) is Relation-like set
K19(K20( the carrier of f, the carrier of f)) is set
G0 is set
g0 is set
[G0,g0] is set
[g0,G0] is set
dom L is Element of K19( the carrier of P)
a is Element of the carrier of f
x is set
L . x is set
I0 is Element of the carrier of f
y is set
L . y is set
n0 is Element of the carrier of P
M0 is Element of the carrier of P
G0 is set
[G0,G0] is set
g0 is Element of the carrier of f
g0 is set
dom L is Element of K19( the carrier of P)
L . g0 is set
G0 is strongly_connected Element of K19( the carrier of f)
the set is set
{ the set } is non empty set
K20({ the set },{ the set }) is Relation-like set
K19(K20({ the set },{ the set })) is set
id { the set } is Relation-like { the set } -defined { the set } -valued Function-like one-to-one non empty V14({ the set }) reflexive symmetric antisymmetric transitive Element of K19(K20({ the set },{ the set }))
h is Relation-like { the set } -defined { the set } -valued Element of K19(K20({ the set },{ the set }))
L is Relation-like { the set } -defined { the set } -valued V14({ the set }) reflexive antisymmetric transitive Element of K19(K20({ the set },{ the set }))
RelStr(# { the set },L #) is non empty V45() V46() 1 -element strict V55() reflexive transitive antisymmetric with_suprema with_infima V162() lower-bounded upper-bounded V168() RelStr
g0 is non empty V45() V46() 1 -element strict V55() reflexive transitive antisymmetric with_suprema with_infima V162() lower-bounded upper-bounded V168() RelStr
the carrier of g0 is non empty V12() V31() set
K19( the carrier of g0) is set
G0 is strongly_connected Element of K19( the carrier of g0)
p0 is Element of the carrier of g0
g0 is Element of the carrier of g0
g0 is Element of the carrier of g0
P is RelStr
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K19( the carrier of P) is set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
h is non empty strongly_connected Element of K19( the carrier of P)
"\/" (h,P) is Element of the carrier of P
L is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
L .: h is Element of K19( the carrier of f)
K19( the carrier of f) is set
"\/" ((L .: h),f) is Element of the carrier of f
L . ("\/" (h,P)) is Element of the carrier of f
g0 is non empty strongly_connected Element of K19( the carrier of f)
g0 is Element of the carrier of f
dom L is Element of K19( the carrier of P)
a is set
L . a is set
I0 is Element of the carrier of P
P is non empty V55() reflexive transitive antisymmetric RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
iter (f,0) is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
h is Element of the carrier of P
(iter (f,0)) . h is Element of the carrier of P
id the carrier of P is Relation-like the carrier of P -defined the carrier of P -valued Function-like one-to-one non empty V14( the carrier of P) reflexive symmetric antisymmetric transitive Element of K19(K20( the carrier of P, the carrier of P))
(id the carrier of P) . h is set
P is non empty V55() reflexive transitive antisymmetric RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
h is Element of the carrier of P
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (f,b₂)) . h } is set
iter (f,0) is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
(iter (f,0)) . h is Element of the carrier of P
P is V24() V25() V26() V30() V117() ext-real non negative V121() set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of f, the carrier of f) is Relation-like set
K19(K20( the carrier of f, the carrier of f)) is set
h is Element of the carrier of f
L is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of f, the carrier of f))
iter (L,P) is Relation-like Function-like set
(iter (L,P)) . h is set
p0 is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of f, the carrier of f))
p0 . h is Element of the carrier of f
P is V24() V25() V26() V30() V117() ext-real non negative V121() set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of f, the carrier of f) is Relation-like set
K19(K20( the carrier of f, the carrier of f)) is set
h is Element of the carrier of f
L is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of f, the carrier of f))
iter (L,P) is Relation-like Function-like set
(iter (L,P)) * L is Relation-like the carrier of f -valued Function-like set
((iter (L,P)) * L) . h is set
(iter (L,P)) . h is set
L . ((iter (L,P)) . h) is set
L * (iter (L,P)) is Relation-like the carrier of f -defined Function-like set
(L * (iter (L,P))) . h is set
L . h is Element of the carrier of f
(iter (L,P)) . (L . h) is set
p0 is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of f, the carrier of f))
L * p0 is Relation-like the carrier of f -defined the carrier of f -valued Function-like Element of K19(K20( the carrier of f, the carrier of f))
(L * p0) . h is set
p0 . h is Element of the carrier of f
L . (p0 . h) is Element of the carrier of f
p0 * L is Relation-like the carrier of f -defined the carrier of f -valued Function-like Element of K19(K20( the carrier of f, the carrier of f))
(p0 * L) . h is set
p0 . (L . h) is Element of the carrier of f
P is V24() V25() V26() V30() V117() ext-real non negative V121() set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of f, the carrier of f) is Relation-like set
K19(K20( the carrier of f, the carrier of f)) is set
h is Element of the carrier of f
L is Element of the carrier of f
g0 is Element of the carrier of f
p0 is Element of the carrier of f
G0 is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of f, the carrier of f))
iter (G0,P) is Relation-like Function-like set
(iter (G0,P)) . h is set
(iter (G0,P)) . L is set
iter (G0,0) is Relation-like Function-like set
g0 is Element of the carrier of f
(iter (G0,0)) . g0 is set
a is Element of the carrier of f
(iter (G0,0)) . a is set
I0 is Element of the carrier of f
x is Element of the carrier of f
iter (G0,0) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of f, the carrier of f))
(iter (G0,0)) . g0 is Element of the carrier of f
(iter (G0,0)) . a is Element of the carrier of f
g0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (G0,g0) is Relation-like Function-like set
g0 + 1 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (G0,(g0 + 1)) is Relation-like Function-like set
a is Element of the carrier of f
(iter (G0,(g0 + 1))) . a is set
I0 is Element of the carrier of f
(iter (G0,(g0 + 1))) . I0 is set
x is Element of the carrier of f
y is Element of the carrier of f
(iter (G0,g0)) . a is set
(iter (G0,g0)) . I0 is set
n0 is Element of the carrier of f
M0 is Element of the carrier of f
(iter (G0,g0)) * G0 is Relation-like the carrier of f -valued Function-like set
G0 . ((iter (G0,g0)) . a) is set
G0 . ((iter (G0,g0)) . I0) is set
a is Element of the carrier of f
I0 is Element of the carrier of f
x is Element of the carrier of f
(iter (G0,(g0 + 1))) . a is set
y is Element of the carrier of f
(iter (G0,(g0 + 1))) . I0 is set
P is V24() V25() V26() V30() V117() ext-real non negative V121() set
f is V24() V25() V26() V30() V117() ext-real non negative V121() set
P + f is V24() V25() V26() V30() V117() ext-real non negative V121() set
h is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of h is non empty set
K20( the carrier of h, the carrier of h) is Relation-like set
K19(K20( the carrier of h, the carrier of h)) is set
L is Element of the carrier of h
g0 is Element of the carrier of h
p0 is Element of the carrier of h
G0 is Element of the carrier of h
g0 is Relation-like the carrier of h -defined the carrier of h -valued Function-like quasi_total monotone Element of K19(K20( the carrier of h, the carrier of h))
g0 . g0 is Element of the carrier of h
iter (g0,P) is Relation-like Function-like set
(iter (g0,P)) . g0 is set
iter (g0,(P + f)) is Relation-like Function-like set
(iter (g0,(P + f))) . g0 is set
P + 0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (g0,(P + 0)) is Relation-like Function-like set
I0 is Element of the carrier of h
a is Element of the carrier of h
g0 . a is Element of the carrier of h
x is Element of the carrier of h
(iter (g0,P)) . a is set
y is Element of the carrier of h
(iter (g0,(P + 0))) . a is set
a is V24() V25() V26() V30() V117() ext-real non negative V121() set
P + a is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (g0,(P + a)) is Relation-like Function-like set
a + 1 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
P + (a + 1) is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (g0,(P + (a + 1))) is Relation-like Function-like set
I0 is Element of the carrier of h
g0 . I0 is Element of the carrier of h
(iter (g0,P)) . I0 is set
(iter (g0,(P + (a + 1)))) . I0 is set
x is Element of the carrier of h
y is Element of the carrier of h
n0 is Element of the carrier of h
(iter (g0,(P + a))) . I0 is set
M0 is Element of the carrier of h
(P + a) + 1 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (g0,((P + a) + 1)) is Relation-like Function-like set
g0 * (iter (g0,(P + a))) is Relation-like the carrier of h -defined Function-like set
(iter (g0,(P + a))) . x is set
x is Element of the carrier of h
I0 is Element of the carrier of h
g0 . I0 is Element of the carrier of h
y is Element of the carrier of h
(iter (g0,P)) . I0 is set
n0 is Element of the carrier of h
(iter (g0,(P + (a + 1)))) . I0 is set
P is V24() V25() V26() V30() V117() ext-real non negative V121() set
f is V24() V25() V26() V30() V117() ext-real non negative V121() set
h is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of h is non empty set
K20( the carrier of h, the carrier of h) is Relation-like set
K19(K20( the carrier of h, the carrier of h)) is set
L is Element of the carrier of h
g0 is Element of the carrier of h
p0 is Element of the carrier of h
G0 is Element of the carrier of h
g0 is Relation-like the carrier of h -defined the carrier of h -valued Function-like quasi_total monotone Element of K19(K20( the carrier of h, the carrier of h))
g0 . g0 is Element of the carrier of h
iter (g0,P) is Relation-like Function-like set
(iter (g0,P)) . g0 is set
iter (g0,f) is Relation-like Function-like set
(iter (g0,f)) . g0 is set
a is V24() V25() V26() V30() V117() ext-real non negative V121() set
P + a is V24() V25() V26() V30() V117() ext-real non negative V121() set
P is V24() V25() V26() V30() V117() ext-real non negative V121() set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of f, the carrier of f) is Relation-like set
K19(K20( the carrier of f, the carrier of f)) is set
h is Element of the carrier of f
L is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of f, the carrier of f))
iter (L,P) is Relation-like Function-like set
(iter (L,P)) . h is set
iter (L,0) is Relation-like Function-like set
g0 is Element of the carrier of f
(iter (L,0)) . g0 is set
g0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (L,g0) is Relation-like Function-like set
g0 + 1 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (L,(g0 + 1)) is Relation-like Function-like set
p0 is Element of the carrier of f
(iter (L,(g0 + 1))) . p0 is set
(iter (L,g0)) * L is Relation-like the carrier of f -valued Function-like set
(iter (L,g0)) . p0 is set
L . ((iter (L,g0)) . p0) is set
L . p0 is Element of the carrier of f
p0 is Element of the carrier of f
(iter (L,(g0 + 1))) . p0 is set
P is V24() V25() V26() V30() V117() ext-real non negative V121() set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of f, the carrier of f) is Relation-like set
K19(K20( the carrier of f, the carrier of f)) is set
h is Element of the carrier of f
L is Element of the carrier of f
g0 is Element of the carrier of f
p0 is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of f, the carrier of f))
iter (p0,P) is Relation-like Function-like set
(iter (p0,P)) . L is set
G0 is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of f, the carrier of f))
iter (G0,P) is Relation-like Function-like set
(iter (G0,P)) . L is set
iter (p0,0) is Relation-like Function-like set
iter (G0,0) is Relation-like Function-like set
g0 is Element of the carrier of f
(iter (p0,0)) . g0 is set
(iter (G0,0)) . g0 is set
a is Element of the carrier of f
I0 is Element of the carrier of f
iter (p0,0) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of f, the carrier of f))
(iter (p0,0)) . g0 is Element of the carrier of f
iter (G0,0) is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of f, the carrier of f))
(iter (G0,0)) . g0 is Element of the carrier of f
g0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (p0,g0) is Relation-like Function-like set
iter (G0,g0) is Relation-like Function-like set
g0 + 1 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (p0,(g0 + 1)) is Relation-like Function-like set
iter (G0,(g0 + 1)) is Relation-like Function-like set
a is Element of the carrier of f
(iter (p0,(g0 + 1))) . a is set
(iter (G0,(g0 + 1))) . a is set
I0 is Element of the carrier of f
x is Element of the carrier of f
(iter (p0,g0)) . a is set
(iter (G0,g0)) . a is set
n0 is Element of the carrier of f
p0 . n0 is Element of the carrier of f
y is Element of the carrier of f
(iter (p0,g0)) * p0 is Relation-like the carrier of f -valued Function-like set
p0 . y is Element of the carrier of f
(iter (G0,g0)) * G0 is Relation-like the carrier of f -valued Function-like set
G0 . n0 is Element of the carrier of f
I0 is Element of the carrier of f
a is Element of the carrier of f
(iter (p0,(g0 + 1))) . a is set
x is Element of the carrier of f
(iter (G0,(g0 + 1))) . a is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
Bottom P is Element of the carrier of P
K19( the carrier of P) is set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
(P,f,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (f,b₂)) . (Bottom P) } is set
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued V14( the carrier of P) reflexive antisymmetric transitive Element of K19(K20( the carrier of P, the carrier of P))
p0 is set
G0 is Element of the carrier of P
g0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,g0) is Relation-like Function-like set
(iter (f,g0)) . (Bottom P) is set
p0 is set
p0 is Element of K19( the carrier of P)
G0 is set
g0 is set
[G0,g0] is set
[g0,G0] is set
a is Element of the carrier of P
x is Element of the carrier of P
I0 is Element of the carrier of P
y is Element of the carrier of P
n0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,n0) is Relation-like Function-like set
(iter (f,n0)) . (Bottom P) is set
n0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,n0) is Relation-like Function-like set
(iter (f,n0)) . (Bottom P) is set
M0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,M0) is Relation-like Function-like set
(iter (f,M0)) . (Bottom P) is set
M0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,M0) is Relation-like Function-like set
(iter (f,M0)) . (Bottom P) is set
iter (f,1) is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
(iter (f,1)) . (Bottom P) is Element of the carrier of P
f . (Bottom P) is Element of the carrier of P
M0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,M0) is Relation-like Function-like set
(iter (f,M0)) . (Bottom P) is set
k is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,k) is Relation-like Function-like set
(iter (f,k)) . (Bottom P) is set
G0 is set
[G0,G0] is set
g0 is Element of the carrier of P
G0 is strongly_connected Element of K19( the carrier of P)
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
Bottom P is Element of the carrier of P
(P,f,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (f,b₂)) . (Bottom P) } is set
K19( the carrier of P) is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
(P,f) is non empty strongly_connected Element of K19( the carrier of P)
K19( the carrier of P) is set
Bottom P is Element of the carrier of P
(P,f,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (f,b₂)) . (Bottom P) } is set
"\/" ((P,f),P) is Element of the carrier of P
f .: (P,f) is Element of K19( the carrier of P)
"\/" ((f .: (P,f)),P) is Element of the carrier of P
h is non empty strongly_connected Element of K19( the carrier of P)
"\/" (h,P) is Element of the carrier of P
G0 is Element of the carrier of P
g0 is Element of the carrier of P
a is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,a) is Relation-like Function-like set
(iter (f,a)) . (Bottom P) is set
a is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,a) is Relation-like Function-like set
(iter (f,a)) . (Bottom P) is set
I0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
1 + I0 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,I0) is Relation-like Function-like set
(iter (f,I0)) . (Bottom P) is set
x is Element of the carrier of P
dom f is Element of K19( the carrier of P)
(iter (f,I0)) * f is Relation-like the carrier of P -valued Function-like set
((iter (f,I0)) * f) . (Bottom P) is set
f . x is Element of the carrier of P
I0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,I0) is Relation-like Function-like set
(iter (f,I0)) . (Bottom P) is set
G0 is Element of the carrier of P
dom f is Element of K19( the carrier of P)
g0 is set
f . g0 is set
a is Element of the carrier of P
I0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,I0) is Relation-like Function-like set
(iter (f,I0)) . (Bottom P) is set
I0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,I0) is Relation-like Function-like set
(iter (f,I0)) . (Bottom P) is set
I0 + 1 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
(iter (f,I0)) * f is Relation-like the carrier of P -valued Function-like set
((iter (f,I0)) * f) . (Bottom P) is set
iter (f,(I0 + 1)) is Relation-like Function-like set
(iter (f,(I0 + 1))) . (Bottom P) is set
y is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,y) is Relation-like Function-like set
(iter (f,y)) . (Bottom P) is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
(P,f) is non empty strongly_connected Element of K19( the carrier of P)
K19( the carrier of P) is set
Bottom P is Element of the carrier of P
(P,f,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (f,b₂)) . (Bottom P) } is set
"\/" ((P,f),P) is Element of the carrier of P
h is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
(P,h) is non empty strongly_connected Element of K19( the carrier of P)
(P,h,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (h,b₂)) . (Bottom P) } is set
"\/" ((P,h),P) is Element of the carrier of P
p0 is Element of the carrier of P
G0 is Element of the carrier of P
g0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,g0) is Relation-like Function-like set
(iter (f,g0)) . (Bottom P) is set
g0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,g0) is Relation-like Function-like set
(iter (f,g0)) . (Bottom P) is set
iter (h,g0) is Relation-like Function-like set
(iter (h,g0)) . (Bottom P) is set
a is Element of the carrier of P
I0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,I0) is Relation-like Function-like set
(iter (f,I0)) . (Bottom P) is set
P is non empty V55() reflexive transitive antisymmetric RelStr
the carrier of P is non empty set
f is non empty V55() reflexive transitive antisymmetric RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K19( the carrier of P) is set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
h is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
L is non empty strongly_connected Element of K19( the carrier of P)
"\/" (L,P) is Element of the carrier of P
h . ("\/" (L,P)) is Element of the carrier of f
h .: L is Element of K19( the carrier of f)
K19( the carrier of f) is set
"\/" ((h .: L),f) is Element of the carrier of f
L is non empty strongly_connected Element of K19( the carrier of P)
"\/" (L,P) is Element of the carrier of P
h . ("\/" (L,P)) is Element of the carrier of f
h .: L is Element of K19( the carrier of f)
K19( the carrier of f) is set
"\/" ((h .: L),f) is Element of the carrier of f
L is non empty strongly_connected Element of K19( the carrier of P)
K19( the carrier of f) is set
h .: L is Element of K19( the carrier of f)
g0 is non empty strongly_connected Element of K19( the carrier of f)
"\/" (L,P) is Element of the carrier of P
h . ("\/" (L,P)) is Element of the carrier of f
"\/" (g0,f) is Element of the carrier of f
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
h is Element of the carrier of P
f --> h is Relation-like the carrier of f -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of f, the carrier of P))
the carrier of f is non empty set
K20( the carrier of f, the carrier of P) is Relation-like set
K19(K20( the carrier of f, the carrier of P)) is set
K231( the carrier of P, the carrier of f,h) is Relation-like the carrier of f -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of f, the carrier of P))
K19( the carrier of f) is set
g0 is non empty strongly_connected Element of K19( the carrier of f)
"\/" (g0,f) is Element of the carrier of f
(f --> h) . ("\/" (g0,f)) is Element of the carrier of P
(f --> h) .: g0 is Element of K19( the carrier of P)
K19( the carrier of P) is set
"\/" (((f --> h) .: g0),P) is Element of the carrier of P
G0 is Element of the carrier of P
dom (f --> h) is Element of K19( the carrier of f)
g0 is set
(f --> h) . g0 is set
G0 is Element of the carrier of P
g0 is set
dom (f --> h) is Element of K19( the carrier of f)
(f --> h) . g0 is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
the Element of the carrier of f is Element of the carrier of f
P --> the Element of the carrier of f is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
K231( the carrier of f, the carrier of P, the Element of the carrier of f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
h is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K19( the carrier of P) is set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
h is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
L is non empty strongly_connected Element of K19( the carrier of P)
"\/" (L,P) is Element of the carrier of P
h . ("\/" (L,P)) is Element of the carrier of f
h .: L is Element of K19( the carrier of f)
K19( the carrier of f) is set
"\/" ((h .: L),f) is Element of the carrier of f
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Element of the carrier of P
h is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
(P,h) is non empty strongly_connected Element of K19( the carrier of P)
K19( the carrier of P) is set
Bottom P is Element of the carrier of P
(P,h,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (h,b₂)) . (Bottom P) } is set
"\/" ((P,h),P) is Element of the carrier of P
dom h is Element of K19( the carrier of P)
h .: (P,h) is Element of K19( the carrier of P)
h . f is Element of the carrier of P
L is non empty strongly_connected Element of K19( the carrier of P)
"\/" (L,P) is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Element of the carrier of P
h is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
(P,h) is non empty strongly_connected Element of K19( the carrier of P)
K19( the carrier of P) is set
Bottom P is Element of the carrier of P
(P,h,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (h,b₂)) . (Bottom P) } is set
"\/" ((P,h),P) is Element of the carrier of P
L is Element of the carrier of P
G0 is Element of the carrier of P
g0 is Element of the carrier of P
a is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (h,a) is Relation-like Function-like set
(iter (h,a)) . (Bottom P) is set
a is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (h,a) is Relation-like Function-like set
(iter (h,a)) . (Bottom P) is set
(iter (h,a)) . L is set
I0 is Element of the carrier of P
L is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
(P,f) is non empty strongly_connected Element of K19( the carrier of P)
K19( the carrier of P) is set
Bottom P is Element of the carrier of P
(P,f,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (f,b₂)) . (Bottom P) } is set
"\/" ((P,f),P) is Element of the carrier of P
L is Element of the carrier of P
h is Element of the carrier of P
L is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P,f) is Element of the carrier of P
(P,f) is non empty strongly_connected Element of K19( the carrier of P)
K19( the carrier of P) is set
Bottom P is Element of the carrier of P
(P,f,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (f,b₂)) . (Bottom P) } is set
"\/" ((P,f),P) is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
h is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P,f) is Element of the carrier of P
(P,h) is Element of the carrier of P
(P,f) is non empty strongly_connected Element of K19( the carrier of P)
K19( the carrier of P) is set
Bottom P is Element of the carrier of P
(P,f,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (f,b₂)) . (Bottom P) } is set
"\/" ((P,f),P) is Element of the carrier of P
(P,h) is non empty strongly_connected Element of K19( the carrier of P)
(P,h,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (h,b₂)) . (Bottom P) } is set
"\/" ((P,h),P) is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
the Element of the carrier of f is Element of the carrier of f
P --> the Element of the carrier of f is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
K231( the carrier of f, the carrier of P, the Element of the carrier of f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
h is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
L is Element of the carrier of P
h . L is Element of the carrier of f
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
h is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
L is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
p0 is Element of the carrier of P
h . p0 is Element of the carrier of f
g0 . p0 is Element of the carrier of f
G0 is Element of the carrier of f
g0 is Element of the carrier of f
L . p0 is Element of the carrier of f
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
h is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
L is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
g0 is set
h . g0 is set
L . g0 is set
p0 is Element of the carrier of P
h . p0 is Element of the carrier of f
L . p0 is Element of the carrier of f
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
L is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
g0 is set
p0 is set
[g0,p0] is set
G0 is set
g0 is set
a is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
I0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
[G0,g0] is set
L is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
g0 is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
p0 is Element of (P,f)
G0 is Element of (P,f)
[p0,G0] is set
g0 is Element of (P,f)
a is Element of (P,f)
I0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
x is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
[g0,a] is set
p0 is Element of (P,f)
G0 is Element of (P,f)
[p0,G0] is set
g0 is Element of (P,f)
a is Element of (P,f)
I0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
x is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
[g0,a] is set
p0 is set
G0 is set
[p0,G0] is set
g0 is set
a is set
I0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
x is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
[g0,a] is set
y is set
n0 is set
[y,n0] is set
M0 is set
M0 is set
k is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
z1 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
[M0,M0] is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
field (P,f) is set
dom (P,f) is set
rng (P,f) is set
(dom (P,f)) \/ (rng (P,f)) is set
(P,f) \/ (P,f) is non empty set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
L is set
[L,L] is set
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f)
p0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
p0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
g0 is set
p0 is set
[g0,p0] is set
G0 is set
[p0,G0] is set
[g0,G0] is set
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
a is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
I0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
x is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
L is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
g0 is set
p0 is set
[g0,p0] is set
[p0,g0] is set
G0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
a is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
I0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
field (P,f) is set
dom (P,f) is set
rng (P,f) is set
(dom (P,f)) \/ (rng (P,f)) is set
h is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
field h is set
dom h is set
rng h is set
(dom h) \/ (rng h) is set
L is set
[L,L] is set
field (P,f) is set
dom (P,f) is set
rng (P,f) is set
(dom (P,f)) \/ (rng (P,f)) is set
g0 is set
p0 is set
[g0,p0] is set
G0 is set
[p0,G0] is set
[g0,G0] is set
field (P,f) is set
dom (P,f) is set
rng (P,f) is set
(dom (P,f)) \/ (rng (P,f)) is set
L is Relation-like (P,f) -defined (P,f) -valued Element of K19(K20((P,f),(P,f)))
g0 is set
p0 is set
[g0,p0] is set
[p0,g0] is set
field L is set
dom L is set
rng L is set
(dom L) \/ (rng L) is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the InternalRel of RelStr(# (P,f),(P,f) #) is Relation-like the carrier of RelStr(# (P,f),(P,f) #) -defined the carrier of RelStr(# (P,f),(P,f) #) -valued Element of K19(K20( the carrier of RelStr(# (P,f),(P,f) #), the carrier of RelStr(# (P,f),(P,f) #)))
the carrier of RelStr(# (P,f),(P,f) #) is non empty set
K20( the carrier of RelStr(# (P,f),(P,f) #), the carrier of RelStr(# (P,f),(P,f) #)) is Relation-like set
K19(K20( the carrier of RelStr(# (P,f),(P,f) #), the carrier of RelStr(# (P,f),(P,f) #))) is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
K19( the carrier of (P,f)) is set
h is non empty strongly_connected Element of K19( the carrier of (P,f))
L is Element of the carrier of P
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . L ) } is set
K19( the carrier of f) is set
the InternalRel of f is Relation-like the carrier of f -defined the carrier of f -valued V14( the carrier of f) reflexive antisymmetric transitive Element of K19(K20( the carrier of f, the carrier of f))
K20( the carrier of f, the carrier of f) is Relation-like set
K19(K20( the carrier of f, the carrier of f)) is set
G0 is set
g0 is Element of the carrier of f
I0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
I0 . L is Element of the carrier of f
a is Element of the carrier of f
G0 is Element of K19( the carrier of f)
g0 is set
a is set
[g0,a] is set
[a,g0] is set
I0 is Element of the carrier of f
x is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
x . L is Element of the carrier of f
x is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
x . L is Element of the carrier of f
y is Element of the carrier of f
n0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
n0 . L is Element of the carrier of f
n0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
n0 . L is Element of the carrier of f
the InternalRel of (P,f) is Relation-like the carrier of (P,f) -defined the carrier of (P,f) -valued V14( the carrier of (P,f)) reflexive antisymmetric transitive Element of K19(K20( the carrier of (P,f), the carrier of (P,f)))
K20( the carrier of (P,f), the carrier of (P,f)) is Relation-like set
K19(K20( the carrier of (P,f), the carrier of (P,f))) is set
[x,n0] is set
M0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
k is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
z1 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
z1 . L is Element of the carrier of f
M1 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
M1 . L is Element of the carrier of f
[n0,x] is set
M0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
k is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
z1 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
z1 . L is Element of the carrier of f
M1 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
M1 . L is Element of the carrier of f
[x,n0] is set
[n0,x] is set
g0 is set
[g0,g0] is set
a is Element of the carrier of f
a is set
I0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f)
x is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
x is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
x . L is Element of the carrier of f
y is Element of the carrier of f
g0 is strongly_connected Element of K19( the carrier of f)
n0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
K19( the carrier of (P,f)) is set
K19( the carrier of f) is set
h is non empty strongly_connected Element of K19( the carrier of (P,f))
p0 is set
G0 is Element of the carrier of P
(P,f,h,G0) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . G0 ) } is set
g0 is non empty strongly_connected Element of K19( the carrier of f)
"\/" (g0,f) is Element of the carrier of f
I0 is Element of the carrier of P
x is non empty strongly_connected Element of K19( the carrier of f)
(P,f,h,I0) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . I0 ) } is set
"\/" (x,f) is Element of the carrier of f
p0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
g0 is non empty strongly_connected Element of K19( the carrier of f)
G0 is Element of the carrier of P
(P,f,h,G0) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . G0 ) } is set
p0 . G0 is Element of the carrier of f
"\/" (g0,f) is Element of the carrier of f
L is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
G0 is set
L . G0 is set
g0 . G0 is set
g0 is Element of the carrier of P
(P,f,h,g0) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . g0 ) } is set
a is non empty strongly_connected Element of K19( the carrier of f)
"\/" (a,f) is Element of the carrier of f
G0 is non empty strongly_connected Element of K19( the carrier of f)
p0 is Element of the carrier of P
(P,f,h,p0) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . p0 ) } is set
L . p0 is Element of the carrier of f
"\/" (G0,f) is Element of the carrier of f
a is non empty strongly_connected Element of K19( the carrier of f)
g0 is Element of the carrier of P
(P,f,h,g0) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . g0 ) } is set
g0 . g0 is Element of the carrier of f
"\/" (a,f) is Element of the carrier of f
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
K19( the carrier of (P,f)) is set
h is non empty strongly_connected Element of K19( the carrier of (P,f))
(P,f,h) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
L is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
g0 is Element of the carrier of P
L . g0 is Element of the carrier of f
p0 is Element of the carrier of P
L . p0 is Element of the carrier of f
G0 is Element of the carrier of f
g0 is Element of the carrier of f
K19( the carrier of f) is set
(P,f,h,g0) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . g0 ) } is set
(P,f,h,p0) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . p0 ) } is set
a is non empty strongly_connected Element of K19( the carrier of f)
I0 is non empty strongly_connected Element of K19( the carrier of f)
"\/" (a,f) is Element of the carrier of f
"\/" (I0,f) is Element of the carrier of f
x is Element of the carrier of f
y is Element of the carrier of f
n0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
n0 . g0 is Element of the carrier of f
n0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
n0 . g0 is Element of the carrier of f
n0 . p0 is Element of the carrier of f
M0 is Element of the carrier of f
M0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
M0 . g0 is Element of the carrier of f
G0 is Element of the carrier of f
g0 is Element of the carrier of f
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K19( the carrier of P) is set
f is non empty strongly_connected Element of K19( the carrier of P)
"\/" (f,P) is Element of the carrier of P
h is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K19( the carrier of P) is set
f is non empty strongly_connected Element of K19( the carrier of P)
"\/" (f,P) is Element of the carrier of P
h is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
K19( the carrier of (P,f)) is set
h is non empty strongly_connected Element of K19( the carrier of (P,f))
(P,f,h) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
K19( the carrier of P) is set
L is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
g0 is non empty strongly_connected Element of K19( the carrier of P)
"\/" (g0,P) is Element of the carrier of P
L . ("\/" (g0,P)) is Element of the carrier of f
L .: g0 is Element of K19( the carrier of f)
K19( the carrier of f) is set
"\/" ((L .: g0),f) is Element of the carrier of f
p0 is non empty strongly_connected Element of K19( the carrier of f)
"\/" (p0,f) is Element of the carrier of f
(P,f,h,("\/" (g0,P))) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . ("\/" (g0,P)) ) } is set
"\/" ((P,f,h,("\/" (g0,P))),f) is Element of the carrier of f
I0 is Element of the carrier of f
x is Element of the carrier of f
y is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
y . ("\/" (g0,P)) is Element of the carrier of f
y is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
y . ("\/" (g0,P)) is Element of the carrier of f
y .: g0 is Element of K19( the carrier of f)
n0 is non empty strongly_connected Element of K19( the carrier of f)
"\/" (n0,f) is Element of the carrier of f
M0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
M0 . ("\/" (g0,P)) is Element of the carrier of f
M0 is Element of the carrier of f
dom y is Element of K19( the carrier of P)
M0 is set
y . M0 is set
k is Element of the carrier of P
(P,f,h,k) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . k ) } is set
L . k is Element of the carrier of f
"\/" ((P,f,h,k),f) is Element of the carrier of f
dom L is Element of K19( the carrier of P)
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
K19( the carrier of (P,f)) is set
h is non empty strongly_connected Element of K19( the carrier of (P,f))
(P,f,h) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
K19( the carrier of (P,f)) is set
h is non empty strongly_connected Element of K19( the carrier of (P,f))
(P,f,h) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
K19( the carrier of (P,f)) is set
h is non empty strongly_connected Element of K19( the carrier of (P,f))
L is set
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f)
p0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
K19( the carrier of (P,f)) is set
h is non empty strongly_connected Element of K19( the carrier of (P,f))
(P,f,h) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
"\/" (h,(P,f)) is Element of the carrier of (P,f)
p0 is Element of the carrier of (P,f)
G0 is Element of the carrier of (P,f)
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
I0 is Element of the carrier of P
g0 . I0 is Element of the carrier of f
(P,f,h) . I0 is Element of the carrier of f
x is Element of the carrier of f
y is Element of the carrier of f
(P,f,h,I0) is non empty strongly_connected Element of K19( the carrier of f)
K19( the carrier of f) is set
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . I0 ) } is set
n0 is non empty strongly_connected Element of K19( the carrier of f)
"\/" (n0,f) is Element of the carrier of f
a is Element of the carrier of (P,f)
[a,p0] is set
G0 is Element of the carrier of (P,f)
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f)
a is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
a is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
I0 is Element of the carrier of P
(P,f,h) . I0 is Element of the carrier of f
a . I0 is Element of the carrier of f
x is Element of the carrier of f
y is Element of the carrier of f
K19( the carrier of f) is set
(P,f,h,I0) is non empty strongly_connected Element of K19( the carrier of f)
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st
( b₂ in h & b₁ = b₂ . I0 ) } is set
n0 is non empty strongly_connected Element of K19( the carrier of f)
M0 is Element of the carrier of f
M0 is Element of the carrier of f
k is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
k . I0 is Element of the carrier of f
k is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
k . I0 is Element of the carrier of f
z1 is Element of the carrier of (P,f)
[z1,G0] is set
M1 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
z is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
M is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
M0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
M0 . I0 is Element of the carrier of f
"\/" (n0,f) is Element of the carrier of f
[p0,G0] is set
I0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
Bottom f is Element of the carrier of f
the carrier of f is non empty set
P --> (Bottom f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
the carrier of P is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
K231( the carrier of f, the carrier of P,(Bottom f)) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
the carrier of P is non empty set
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
Bottom f is Element of the carrier of f
P --> (Bottom f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
K231( the carrier of f, the carrier of P,(Bottom f)) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
the carrier of P is non empty set
the carrier of f is non empty set
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
Bottom f is Element of the carrier of f
P --> (Bottom f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
K231( the carrier of f, the carrier of P,(Bottom f)) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
h is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
L is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f)
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
(P,f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
Bottom f is Element of the carrier of f
P --> (Bottom f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
K231( the carrier of f, the carrier of P,(Bottom f)) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
h is Element of the carrier of (P,f)
g0 is Element of the carrier of (P,f)
p0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f)
G0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
G0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
g0 is Element of the carrier of P
(P,f) . g0 is Element of the carrier of f
G0 . g0 is Element of the carrier of f
a is Element of the carrier of f
I0 is Element of the carrier of f
[h,g0] is set
g0 is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,f) is non empty strict V55() reflexive transitive antisymmetric RelStr
(P,f) is non empty set
the carrier of P is non empty set
the carrier of f is non empty set
Funcs ( the carrier of P, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of f
K20( the carrier of P, the carrier of f) is Relation-like set
K19(K20( the carrier of P, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of f) : ex b₂ being Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f)) st b₂ = b₁ } is set
(P,f) is Relation-like (P,f) -defined (P,f) -valued reflexive antisymmetric transitive Element of K19(K20((P,f),(P,f)))
K20((P,f),(P,f)) is Relation-like set
K19(K20((P,f),(P,f))) is set
RelStr(# (P,f),(P,f) #) is non empty strict RelStr
the carrier of (P,f) is non empty set
(P,f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone (P,f) Element of K19(K20( the carrier of P, the carrier of f))
Bottom f is Element of the carrier of f
P --> (Bottom f) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of f))
K231( the carrier of f, the carrier of P,(Bottom f)) is Relation-like the carrier of P -defined the carrier of f -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of f))
L is Element of the carrier of (P,f)
L is Element of the carrier of (P,f)
K19( the carrier of (P,f)) is set
L is strongly_connected Element of K19( the carrier of (P,f))
P is set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(f,f) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(f,f) is non empty set
the carrier of f is non empty set
Funcs ( the carrier of f, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of f, the carrier of f
K20( the carrier of f, the carrier of f) is Relation-like set
K19(K20( the carrier of f, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of f, the carrier of f) : ex b₂ being Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone (f,f) Element of K19(K20( the carrier of f, the carrier of f)) st b₂ = b₁ } is set
(f,f) is Relation-like (f,f) -defined (f,f) -valued reflexive antisymmetric transitive Element of K19(K20((f,f),(f,f)))
K20((f,f),(f,f)) is Relation-like set
K19(K20((f,f),(f,f))) is set
RelStr(# (f,f),(f,f) #) is non empty strict RelStr
the carrier of (f,f) is non empty set
h is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of f, the carrier of f)
L is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone (f,f) Element of K19(K20( the carrier of f, the carrier of f))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
h is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P)
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K20( the carrier of (P,P), the carrier of P) is Relation-like set
K19(K20( the carrier of (P,P), the carrier of P)) is set
L is set
g0 is Element of the carrier of (P,P)
p0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P,p0) is Element of the carrier of P
G0 is Element of the carrier of (P,P)
g0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P,g0) is Element of the carrier of P
L is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of (P,P), the carrier of P))
g0 is Element of the carrier of (P,P)
p0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
L . g0 is Element of the carrier of P
(P,p0) is Element of the carrier of P
f is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of (P,P), the carrier of P))
h is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of (P,P), the carrier of P))
g0 is set
f . g0 is set
h . g0 is set
p0 is Element of the carrier of (P,P)
G0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P,G0) is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
f is Element of the carrier of (P,P)
h is Element of the carrier of (P,P)
[f,h] is set
L is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
g0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
p0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
G0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
g0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
a is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
L is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
g0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P) is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of (P,P), the carrier of P))
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K20( the carrier of (P,P), the carrier of P) is Relation-like set
K19(K20( the carrier of (P,P), the carrier of P)) is set
h is Element of the carrier of (P,P)
L is Element of the carrier of (P,P)
(P) . h is Element of the carrier of P
(P) . L is Element of the carrier of P
g0 is Element of the carrier of P
p0 is Element of the carrier of P
G0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
g0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P,G0) is Element of the carrier of P
(P,g0) is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K19( the carrier of (P,P)) is set
Bottom P is Element of the carrier of P
f is non empty strongly_connected Element of K19( the carrier of (P,P))
h is V24() V25() V26() V30() V117() ext-real non negative V121() set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Element of the carrier of (P,P) ex b₃ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₃ = b₂ & b₂ in f & b₁ = (iter (b₃,h)) . (Bottom P) ) } is set
L is set
g0 is set
p0 is Element of the carrier of P
g0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
G0 is Element of the carrier of (P,P)
iter (g0,h) is Relation-like Function-like set
(iter (g0,h)) . (Bottom P) is set
P is set
f is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(f,f) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(f,f) is non empty set
the carrier of f is non empty set
Funcs ( the carrier of f, the carrier of f) is non empty FUNCTION_DOMAIN of the carrier of f, the carrier of f
K20( the carrier of f, the carrier of f) is Relation-like set
K19(K20( the carrier of f, the carrier of f)) is set
{ b₁ where b₁ is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total Element of Funcs ( the carrier of f, the carrier of f) : ex b₂ being Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone (f,f) Element of K19(K20( the carrier of f, the carrier of f)) st b₂ = b₁ } is set
(f,f) is Relation-like (f,f) -defined (f,f) -valued reflexive antisymmetric transitive Element of K19(K20((f,f),(f,f)))
K20((f,f),(f,f)) is Relation-like set
K19(K20((f,f),(f,f))) is set
RelStr(# (f,f),(f,f) #) is non empty strict RelStr
the carrier of (f,f) is non empty set
K19( the carrier of (f,f)) is set
Bottom f is Element of the carrier of f
h is non empty strongly_connected Element of K19( the carrier of (f,f))
L is V24() V25() V26() V30() V117() ext-real non negative V121() set
{ b₁ where b₁ is Element of the carrier of f : ex b₂ being Element of the carrier of (f,f) ex b₃ being Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone (f,f) Element of K19(K20( the carrier of f, the carrier of f)) st
( b₃ = b₂ & b₂ in h & b₁ = (iter (b₃,L)) . (Bottom f) ) } is set
g0 is set
p0 is Element of the carrier of f
g0 is Relation-like the carrier of f -defined the carrier of f -valued Function-like quasi_total monotone (f,f) Element of K19(K20( the carrier of f, the carrier of f))
G0 is Element of the carrier of (f,f)
iter (g0,L) is Relation-like Function-like set
(iter (g0,L)) . (Bottom f) is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K19( the carrier of (P,P)) is set
Bottom P is Element of the carrier of P
K19( the carrier of P) is set
f is non empty strongly_connected Element of K19( the carrier of (P,P))
h is V24() V25() V26() V30() V117() ext-real non negative V121() set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Element of the carrier of (P,P) ex b₃ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₃ = b₂ & b₂ in f & b₁ = (iter (b₃,h)) . (Bottom P) ) } is set
L is set
g0 is set
p0 is Element of the carrier of (P,P)
G0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
iter (G0,h) is Relation-like Function-like set
(iter (G0,h)) . (Bottom P) is set
g0 is Element of the carrier of P
a is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K19( the carrier of (P,P)) is set
f is non empty strongly_connected Element of K19( the carrier of (P,P))
h is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
L is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
the InternalRel of (P,P) is Relation-like the carrier of (P,P) -defined the carrier of (P,P) -valued V14( the carrier of (P,P)) reflexive antisymmetric transitive Element of K19(K20( the carrier of (P,P), the carrier of (P,P)))
K20( the carrier of (P,P), the carrier of (P,P)) is Relation-like set
K19(K20( the carrier of (P,P), the carrier of (P,P))) is set
[h,L] is set
p0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
G0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
[L,h] is set
p0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
G0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
[h,L] is set
[L,h] is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K19( the carrier of (P,P)) is set
Bottom P is Element of the carrier of P
K19( the carrier of P) is set
f is non empty strongly_connected Element of K19( the carrier of (P,P))
h is V24() V25() V26() V30() V117() ext-real non negative V121() set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Element of the carrier of (P,P) ex b₃ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₃ = b₂ & b₂ in f & b₁ = (iter (b₃,h)) . (Bottom P) ) } is set
L is set
the InternalRel of P is Relation-like the carrier of P -defined the carrier of P -valued V14( the carrier of P) reflexive antisymmetric transitive Element of K19(K20( the carrier of P, the carrier of P))
p0 is non empty Element of K19( the carrier of P)
G0 is set
g0 is set
[G0,g0] is set
[g0,G0] is set
a is Element of the carrier of P
I0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
iter (I0,h) is Relation-like Function-like set
(iter (I0,h)) . (Bottom P) is set
x is Element of the carrier of P
y is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
iter (y,h) is Relation-like Function-like set
(iter (y,h)) . (Bottom P) is set
G0 is set
[G0,G0] is set
g0 is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K20( the carrier of (P,P), the carrier of P) is Relation-like set
K19(K20( the carrier of (P,P), the carrier of P)) is set
K19( the carrier of (P,P)) is set
f is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of (P,P), the carrier of P))
h is non empty strongly_connected Element of K19( the carrier of (P,P))
f .: h is Element of K19( the carrier of P)
K19( the carrier of P) is set
L is set
f . L is set
G0 is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of (P,P), the carrier of P))
dom G0 is Element of K19( the carrier of (P,P))
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
the carrier of P is non empty set
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
(P) is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of (P,P), the carrier of P))
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K20( the carrier of (P,P), the carrier of P) is Relation-like set
K19(K20( the carrier of (P,P), the carrier of P)) is set
Bottom P is Element of the carrier of P
f is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P) . f is set
h is Element of the carrier of P
L is Element of the carrier of P
g0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (f,g0) is Relation-like Function-like set
(iter (f,g0)) . (Bottom P) is set
(P,f,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (f,b₂)) . (Bottom P) } is set
G0 is Element of the carrier of (P,P)
g0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P,g0) is Element of the carrier of P
(P,f) is non empty strongly_connected Element of K19( the carrier of P)
K19( the carrier of P) is set
"\/" ((P,f),P) is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K19( the carrier of (P,P)) is set
K19( the carrier of P) is set
Bottom P is Element of the carrier of P
f is non empty strongly_connected Element of K19( the carrier of (P,P))
h is set
L is V24() V25() V26() V30() V117() ext-real non negative V121() set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Element of the carrier of (P,P) ex b₃ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₃ = b₂ & b₂ in f & b₁ = (iter (b₃,L)) . (Bottom P) ) } is set
g0 is non empty strongly_connected Element of K19( the carrier of P)
p0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of P, the carrier of P))
p0 .: g0 is Element of K19( the carrier of P)
dom p0 is Element of K19( the carrier of P)
G0 is set
p0 . G0 is set
G0 is Element of g0
p0 . G0 is Element of the carrier of P
g0 is Element of the carrier of P
I0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
a is Element of the carrier of (P,P)
iter (I0,L) is Relation-like Function-like set
(iter (I0,L)) . (Bottom P) is set
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
the carrier of (P,P) is non empty set
K19( the carrier of (P,P)) is set
(P) is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of (P,P), the carrier of P))
K20( the carrier of (P,P), the carrier of P) is Relation-like set
K19(K20( the carrier of (P,P), the carrier of P)) is set
f is non empty strongly_connected Element of K19( the carrier of (P,P))
"\/" (f,(P,P)) is Element of the carrier of (P,P)
(P) . ("\/" (f,(P,P))) is Element of the carrier of P
(P) .: f is Element of K19( the carrier of P)
K19( the carrier of P) is set
"\/" (((P) .: f),P) is Element of the carrier of P
h is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of (P,P), the carrier of P))
h . ("\/" (f,(P,P))) is Element of the carrier of P
h .: f is Element of K19( the carrier of P)
"\/" ((h .: f),P) is Element of the carrier of P
G0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P,G0) is Element of the carrier of P
(P,P,f) is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
Bottom P is Element of the carrier of P
g0 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
(P,g0,(Bottom P)) is non empty set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being V24() V25() V26() V30() V117() ext-real non negative V121() set st b₁ = (iter (g0,b₂)) . (Bottom P) } is set
(P,g0) is non empty strongly_connected Element of K19( the carrier of P)
"\/" ((P,g0),P) is Element of the carrier of P
I0 is non empty strongly_connected Element of K19( the carrier of P)
"\/" (I0,P) is Element of the carrier of P
L is non empty strongly_connected Element of K19( the carrier of P)
"\/" (L,P) is Element of the carrier of P
x is Element of the carrier of P
y is Element of the carrier of P
n0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (g0,n0) is Relation-like Function-like set
(iter (g0,n0)) . (Bottom P) is set
n0 is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (g0,n0) is Relation-like Function-like set
(iter (g0,n0)) . (Bottom P) is set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Element of the carrier of (P,P) ex b₃ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₃ = b₂ & b₂ in f & b₁ = (iter (b₃,n0)) . (Bottom P) ) } is set
M0 is non empty strongly_connected Element of K19( the carrier of P)
k is Element of the carrier of P
z1 is Element of the carrier of P
M1 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
iter (M1,n0) is Relation-like Function-like set
(iter (M1,n0)) . (Bottom P) is set
h . M1 is set
M is Element of the carrier of P
"\/" (M0,P) is Element of the carrier of P
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Element of the carrier of (P,P) ex b₃ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₃ = b₂ & b₂ in f & b₁ = (iter (b₃,a₁)) . (Bottom P) ) } is set
iter (g0,0) is Relation-like Function-like set
(iter (g0,0)) . (Bottom P) is set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Element of the carrier of (P,P) ex b₃ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₃ = b₂ & b₂ in f & b₁ = (iter (b₃,0)) . (Bottom P) ) } is set
k is Element of the carrier of P
z1 is non empty strongly_connected Element of K19( the carrier of P)
"\/" (z1,P) is Element of the carrier of P
iter (g0,0) is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of P, the carrier of P))
(iter (g0,0)) . (Bottom P) is Element of the carrier of P
k is V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (g0,k) is Relation-like Function-like set
(iter (g0,k)) . (Bottom P) is set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Element of the carrier of (P,P) ex b₃ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₃ = b₂ & b₂ in f & b₁ = (iter (b₃,k)) . (Bottom P) ) } is set
k + 1 is non empty V24() V25() V26() V30() V117() ext-real non negative V121() set
iter (g0,(k + 1)) is Relation-like Function-like set
(iter (g0,(k + 1))) . (Bottom P) is set
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Element of the carrier of (P,P) ex b₃ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₃ = b₂ & b₂ in f & b₁ = (iter (b₃,(k + 1))) . (Bottom P) ) } is set
z1 is Element of the carrier of P
M1 is non empty strongly_connected Element of K19( the carrier of P)
"\/" (M1,P) is Element of the carrier of P
(iter (g0,k)) * g0 is Relation-like the carrier of P -valued Function-like set
((iter (g0,k)) * g0) . (Bottom P) is set
z is Element of the carrier of P
g0 . z is Element of the carrier of P
M is non empty strongly_connected Element of K19( the carrier of P)
g0 .: M is Element of K19( the carrier of P)
"\/" (M,P) is Element of the carrier of P
g0 . ("\/" (M,P)) is Element of the carrier of P
M0 is non empty strongly_connected Element of K19( the carrier of P)
"\/" (M0,P) is Element of the carrier of P
q is Element of the carrier of P
g is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
iter (g,k) is Relation-like Function-like set
(iter (g,k)) . (Bottom P) is set
g0 . ((iter (g,k)) . (Bottom P)) is set
a1 is Element of the carrier of P
(P,P,f,a1) is non empty strongly_connected Element of K19( the carrier of P)
{ b₁ where b₁ is Element of the carrier of P : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st
( b₂ in f & b₁ = b₂ . a1 ) } is set
W is non empty strongly_connected Element of K19( the carrier of P)
"\/" (W,P) is Element of the carrier of P
q1 is Element of the carrier of P
q2 is Element of the carrier of P
g1 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
g1 . a1 is Element of the carrier of P
g1 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
g1 . a1 is Element of the carrier of P
g . a1 is Element of the carrier of P
a3 is Element of the carrier of (P,P)
(iter (g,k)) * g is Relation-like the carrier of P -valued Function-like set
((iter (g,k)) * g) . (Bottom P) is set
g2 is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
iter (g2,(k + 1)) is Relation-like Function-like set
(iter (g2,(k + 1))) . (Bottom P) is set
iter (g1,k) is Relation-like Function-like set
(iter (g1,k)) . (Bottom P) is set
a2 is Element of the carrier of P
g1 . a2 is Element of the carrier of P
g2 is Element of the carrier of (P,P)
(iter (g1,k)) * g1 is Relation-like the carrier of P -valued Function-like set
((iter (g1,k)) * g1) . (Bottom P) is set
gg is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P))
iter (gg,(k + 1)) is Relation-like Function-like set
(iter (gg,(k + 1))) . (Bottom P) is set
z1 is Element of the carrier of P
M1 is non empty strongly_connected Element of K19( the carrier of P)
"\/" (M1,P) is Element of the carrier of P
P is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty strict V55() reflexive transitive antisymmetric lower-bounded () RelStr
(P,P) is non empty set
the carrier of P is non empty set
Funcs ( the carrier of P, the carrier of P) is non empty FUNCTION_DOMAIN of the carrier of P, the carrier of P
K20( the carrier of P, the carrier of P) is Relation-like set
K19(K20( the carrier of P, the carrier of P)) is set
{ b₁ where b₁ is Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total Element of Funcs ( the carrier of P, the carrier of P) : ex b₂ being Relation-like the carrier of P -defined the carrier of P -valued Function-like quasi_total monotone (P,P) Element of K19(K20( the carrier of P, the carrier of P)) st b₂ = b₁ } is set
(P,P) is Relation-like (P,P) -defined (P,P) -valued reflexive antisymmetric transitive Element of K19(K20((P,P),(P,P)))
K20((P,P),(P,P)) is Relation-like set
K19(K20((P,P),(P,P))) is set
RelStr(# (P,P),(P,P) #) is non empty strict RelStr
(P) is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total Element of K19(K20( the carrier of (P,P), the carrier of P))
the carrier of (P,P) is non empty set
K20( the carrier of (P,P), the carrier of P) is Relation-like set
K19(K20( the carrier of (P,P), the carrier of P)) is set
K19( the carrier of (P,P)) is set
f is Relation-like the carrier of (P,P) -defined the carrier of P -valued Function-like quasi_total monotone Element of K19(K20( the carrier of (P,P), the carrier of P))
h is non empty strongly_connected Element of K19( the carrier of (P,P))
"\/" (h,(P,P)) is Element of the carrier of (P,P)
f . ("\/" (h,(P,P))) is Element of the carrier of P
f .: h is Element of K19( the carrier of P)
K19( the carrier of P) is set
"\/" ((f .: h),P) is Element of the carrier of P