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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(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

(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

( b

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

(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

( b

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

( b

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

( b

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

( b

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

( b

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

( b

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

(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

( b

(P,f,h,p0) is non empty strongly_connected Element of K19( the carrier of f)

{ b

( b

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

(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

( b

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

( b

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

(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