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

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

rng P is set
dom P is set

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

rng P is set
dom P is set
f is V24() V25() V26() V30() V117() ext-real non negative V121() set

dom (iter (P,f)) is set
rng (iter (P,f)) is set

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

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

h is V24() V25() V26() V30() V117() ext-real non negative V121() 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)

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

the carrier of P is non empty set
K19( the carrier of P) is 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
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

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

the carrier of P is non empty set
K19( the carrier of P) is 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
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

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

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
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (f,b2)) . 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

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

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

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

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

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

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

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)) . h is 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

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

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

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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (f,b2)) . () } 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)) . () 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)) . () 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)) . () 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)) . () 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)) . () 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)) . () is Element of the carrier of P
f . () 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)) . () is set
k is V24() V25() V26() V30() V117() ext-real non negative V121() set

(iter (f,k)) . () 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)

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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (f,b2)) . () } is set
K19( the carrier of P) is set

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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (f,b2)) . () } 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 set
a is V24() V25() V26() V30() V117() ext-real non negative V121() set

(iter (f,a)) . () 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)) . () 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) . () 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)) . () 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)) . () 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)) . () 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) . () is set
iter (f,(I0 + 1)) is Relation-like Function-like set
(iter (f,(I0 + 1))) . () is set
y is V24() V25() V26() V30() V117() ext-real non negative V121() set

(iter (f,y)) . () is set

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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (f,b2)) . () } 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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (h,b2)) . () } 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)) . () 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)) . () is set
iter (h,g0) is Relation-like Function-like set
(iter (h,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)) . () is set

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

the carrier of P is non empty set
K19( the carrier of P) is 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
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

the carrier of P is non empty set

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

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

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

the carrier of P is non empty set
K19( the carrier of P) is 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
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

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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (h,b2)) . () } 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

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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (h,b2)) . () } 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 set
a is V24() V25() V26() V30() V117() ext-real non negative V121() set

(iter (h,a)) . () is set
(iter (h,a)) . L is set
I0 is Element of the carrier of P
L is Element of the carrier of P

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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (f,b2)) . () } 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

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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (f,b2)) . () } is set
"\/" ((P,f),P) is Element of the carrier of P

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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (f,b2)) . () } 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,()) is non empty set
{ b1 where b1 is Element of the carrier of P : ex b2 being V24() V25() V26() V30() V117() ext-real non negative V121() set st b1 = (iter (h,b2)) . () } is set
"\/" ((P,h),P) is Element of the carrier of P

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
{ b1 where b1 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 b2 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 b2 = b1 } 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))

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

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

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
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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . 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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . 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)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . 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)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . 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)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . 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)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . 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)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . g0 )
}
is set

g0 . g0 is Element of the carrier of f
"\/" (a,f) is Element of the carrier of f

(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
{ b1 where b1 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 b2 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 b2 = b1 } 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)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . g0 )
}
is set

(P,f,h,p0) is non empty strongly_connected Element of K19( the carrier of f)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . 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

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

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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . ("\/" (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)
{ b1 where b1 is Element of the carrier of f : ex b2 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
( b2 in h & b1 = b2 . 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,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
{ b1 where b1 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 b2 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 b2 = b1 } 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,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
{ b1 where b1 is Relation-like the carrier of P -defined the carrier of f -valued