:: ORDERS_4 semantic presentation

REAL is V35() V36() V37() V41() set
NAT is non trivial ordinal V35() V36() V37() V38() V39() V40() V41() V56() cardinal limit_cardinal Element of K32(REAL)
K32(REAL) is set
COMPLEX is V35() V41() set
NAT is non trivial ordinal V35() V36() V37() V38() V39() V40() V41() V56() cardinal limit_cardinal set
K32(NAT) is non trivial V56() set
{} is empty ordinal natural V24() ext-real non negative V32() V35() V36() V37() V38() V39() V40() V41() V56() V60() cardinal {} -element set
1 is non empty ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
{{},1} is non empty V35() V36() V37() V38() V39() V40() V56() V60() set
K32(NAT) is non trivial V56() set
is non empty trivial V35() V36() V37() V38() V39() V40() V56() V60() 1 -element set
0 is empty ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V41() V56() V60() cardinal {} -element Element of NAT
dom {} is set
rng {} is set

A is RelStr
the carrier of A is set
the InternalRel of A is Relation-like the carrier of A -defined the carrier of A -valued Element of K32(K33( the carrier of A, the carrier of A))
K33( the carrier of A, the carrier of A) is set
K32(K33( the carrier of A, the carrier of A)) is set
f is set
c3 is set
b is set
[f,c3] is set
{f,c3} is non empty V56() set
{f} is non empty trivial V56() 1 -element set
{{f,c3},{f}} is non empty V56() V60() set
[c3,b] is set
{c3,b} is non empty V56() set
{c3} is non empty trivial V56() 1 -element set
{{c3,b},{c3}} is non empty V56() V60() set
[f,b] is set
{f,b} is non empty V56() set
{{f,b},{f}} is non empty V56() V60() set
f is set
c3 is set
[f,c3] is set
{f,c3} is non empty V56() set
{f} is non empty trivial V56() 1 -element set
{{f,c3},{f}} is non empty V56() V60() set
[c3,f] is set
{c3,f} is non empty V56() set
{c3} is non empty trivial V56() 1 -element set
{{c3,f},{c3}} is non empty V56() V60() set
f is set
[f,f] is set
{f,f} is non empty V56() set
{f} is non empty trivial V56() 1 -element set
{{f,f},{f}} is non empty V56() V60() set
A is ()

A is non empty V80() reflexive transitive antisymmetric ()

the carrier of the finite V80() reflexive transitive antisymmetric () is V56() set
A is non empty connected RelStr
f is non empty SubRelStr of A
the carrier of f is non empty set
c3 is Element of the carrier of f
b is Element of the carrier of f
the carrier of A is non empty set
B is Element of the carrier of A
Ab is Element of the carrier of A
A is finite RelStr
f is SubRelStr of A
the carrier of f is set
the carrier of A is V56() set

the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued V28( the carrier of ()) reflexive antisymmetric transitive Element of K32(K33( the carrier of (), the carrier of ()))
the carrier of () is set
K33( the carrier of (), the carrier of ()) is set
K32(K33( the carrier of (), the carrier of ())) is set

K33(f,f) is V56() set
K32(K33(f,f)) is V56() V60() set

K33(A,A) is V56() set
K32(K33(A,A)) is V56() V60() set
c3 is set
() |_2 A is Relation-like set
() /\ K33(A,A) is V56() set
the carrier of () is set
the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued V28( the carrier of ()) reflexive antisymmetric transitive Element of K32(K33( the carrier of (), the carrier of ()))
K33( the carrier of (), the carrier of ()) is set
K32(K33( the carrier of (), the carrier of ())) is set
() |_2 A is Relation-like set
() /\ K33(A,A) is V56() set
the InternalRel of () |_2 the carrier of () is Relation-like set
the InternalRel of () /\ K33( the carrier of (), the carrier of ()) is set
A is RelStr
f is set
c3 is set
f /\ c3 is set
b is set
f \/ c3 is set
the carrier of A is set
Ab is Element of the carrier of A

the carrier of A is non empty set
Top A is Element of the carrier of A
{(Top A)} is non empty trivial V56() 1 -element Element of K32( the carrier of A)
K32( the carrier of A) is set
the carrier of A \ {(Top A)} is Element of K32( the carrier of A)
f is Element of the carrier of A
c3 is Element of the carrier of A
( the carrier of A \ {(Top A)}) \/ {(Top A)} is non empty Element of K32( the carrier of A)
A is RelStr
the carrier of A is set
f is RelStr
the carrier of f is set
K33( the carrier of A, the carrier of f) is set
K32(K33( the carrier of A, the carrier of f)) is set
c3 is Relation-like the carrier of A -defined the carrier of f -valued Function-like V29( the carrier of A, the carrier of f) Element of K32(K33( the carrier of A, the carrier of f))

the carrier of A is set
K32( the carrier of A) is set

the carrier of f is set
K32( the carrier of f) is set
K33( the carrier of A, the carrier of f) is set
K32(K33( the carrier of A, the carrier of f)) is set
c3 is Element of K32( the carrier of A)
b is Element of K32( the carrier of A)

the carrier of () is set

the carrier of () is set
c3 \/ b is Element of K32( the carrier of A)
Ab is Element of K32( the carrier of f)
B is Element of K32( the carrier of f)

the carrier of () is set
K33( the carrier of (), the carrier of ()) is set
K32(K33( the carrier of (), the carrier of ())) is set

the carrier of () is set
K33( the carrier of (), the carrier of ()) is set
K32(K33( the carrier of (), the carrier of ())) is set
Ab \/ B is Element of K32( the carrier of f)
f is Relation-like the carrier of () -defined the carrier of () -valued Function-like V29( the carrier of (), the carrier of ()) Element of K32(K33( the carrier of (), the carrier of ()))
n9 is Relation-like the carrier of () -defined the carrier of () -valued Function-like V29( the carrier of (), the carrier of ()) Element of K32(K33( the carrier of (), the carrier of ()))

dom f is set
b9 is set
(f +* n9) . b9 is set
dom n9 is set
dom (f +* n9) is set
b9 is Relation-like the carrier of A -defined the carrier of f -valued Function-like V29( the carrier of A, the carrier of f) Element of K32(K33( the carrier of A, the carrier of f))
dom n9 is set
dom f is set
dom (f +* n9) is set
(dom f) \/ (dom n9) is set
rng (f +* n9) is set
rng f is set
rng n9 is set
(rng f) \/ (rng n9) is set
b9 is set
X9 is set
f . X9 is set
(f +* n9) . X9 is set
X9 is set
n9 . X9 is set
(f +* n9) . X9 is set
b9 is set
(f +* n9) . b9 is set
X9 is non empty RelStr
the carrier of X9 is non empty set
b9 is non empty RelStr
the carrier of b9 is non empty set
K33( the carrier of X9, the carrier of b9) is set
K32(K33( the carrier of X9, the carrier of b9)) is set
g is Relation-like the carrier of X9 -defined the carrier of b9 -valued Function-like V29( the carrier of X9, the carrier of b9) Element of K32(K33( the carrier of X9, the carrier of b9))
g is Element of the carrier of X9
A2 is Element of the carrier of X9
g . g is Element of the carrier of b9
g . A2 is Element of the carrier of b9
K32( the carrier of b9) is set
K32( the carrier of X9) is set
e is non empty Element of K32( the carrier of X9)
subrelstr e is non empty strict full SubRelStr of X9
the carrier of () is non empty set
g is non empty Element of K32( the carrier of b9)
subrelstr g is non empty strict full SubRelStr of b9
the carrier of () is non empty set
K33( the carrier of (), the carrier of ()) is set
K32(K33( the carrier of (), the carrier of ())) is set
f . g is set
f . A2 is set
f is Element of the carrier of ()
f1 is Element of the carrier of ()
e1 is Relation-like the carrier of () -defined the carrier of () -valued Function-like V29( the carrier of (), the carrier of ()) Element of K32(K33( the carrier of (), the carrier of ()))
e1 . f is Element of the carrier of ()
e1 . f1 is Element of the carrier of ()
K32( the carrier of b9) is set
K32( the carrier of X9) is set
f is non empty Element of K32( the carrier of X9)
subrelstr f is non empty strict full SubRelStr of X9
the carrier of () is non empty set
g is non empty Element of K32( the carrier of b9)
subrelstr g is non empty strict full SubRelStr of b9
the carrier of () is non empty set
K33( the carrier of (), the carrier of ()) is set
K32(K33( the carrier of (), the carrier of ())) is set
f1 is non empty Element of K32( the carrier of X9)
subrelstr f1 is non empty strict full SubRelStr of X9
the carrier of () is non empty set
e is non empty Element of K32( the carrier of b9)
subrelstr e is non empty strict full SubRelStr of b9
the carrier of () is non empty set
K33( the carrier of (), the carrier of ()) is set
K32(K33( the carrier of (), the carrier of ())) is set
e1 is Relation-like the carrier of () -defined the carrier of () -valued Function-like V29( the carrier of (), the carrier of ()) Element of K32(K33( the carrier of (), the carrier of ()))
ax is Element of the carrier of ()
e1 . ax is Element of the carrier of ()
g9 is Relation-like the carrier of () -defined the carrier of () -valued Function-like V29( the carrier of (), the carrier of ()) Element of K32(K33( the carrier of (), the carrier of ()))
ay is Element of the carrier of ()
g9 . ay is Element of the carrier of ()
f . g is set
n9 . A2 is set
n9 . g is set
f . A2 is set
K32( the carrier of b9) is set
K32( the carrier of X9) is set
e is non empty Element of K32( the carrier of X9)
subrelstr e is non empty strict full SubRelStr of X9
the carrier of () is non empty set
g is non empty Element of K32( the carrier of b9)
subrelstr g is non empty strict full SubRelStr of b9
the carrier of () is non empty set
K33( the carrier of (), the carrier of ()) is set
K32(K33( the carrier of (), the carrier of ())) is set
n9 . g is set
n9 . A2 is set
f is Element of the carrier of ()
f1 is Element of the carrier of ()
e1 is Relation-like the carrier of () -defined the carrier of () -valued Function-like V29( the carrier of (), the carrier of ()) Element of K32(K33( the carrier of (), the carrier of ()))
e1 . f is Element of the carrier of ()
e1 . f1 is Element of the carrier of ()
g is Element of the carrier of X9
g . g is Element of the carrier of b9
A2 is Element of the carrier of X9
g . A2 is Element of the carrier of b9
f . g is set
f . A2 is set
f . g is set
n9 . A2 is set
f . A2 is set
n9 . g is set
n9 . g is set
n9 . A2 is set

A + 1 is non empty ordinal natural V24() ext-real non negative V32() V56() cardinal set
InclPoset (A + 1) is non empty strict V80() reflexive transitive antisymmetric RelStr
0 + 1 is non empty ordinal natural V24() ext-real non negative V32() V56() cardinal set

the carrier of f is V56() set
card the carrier of f is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
c3 is non empty finite V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() ()
Top c3 is Element of the carrier of c3
the carrier of c3 is non empty V56() set
Ab is set
{Ab} is non empty trivial V56() 1 -element set

the carrier of c3 --> 0 is Relation-like the carrier of c3 -defined -valued Function-like V29( the carrier of c3,) V56() Element of K32(K33( the carrier of c3,))
is non empty trivial V35() V36() V37() V38() V39() V40() V56() V60() 1 -element set
K33( the carrier of c3,) is V56() set
K32(K33( the carrier of c3,)) is V56() V60() set
rng ( the carrier of c3 --> 0) is V56() set
the carrier of () is non empty set
K33( the carrier of c3, the carrier of ()) is set
K32(K33( the carrier of c3, the carrier of ())) is set
f is Relation-like the carrier of c3 -defined the carrier of () -valued Function-like V29( the carrier of c3, the carrier of ()) V56() Element of K32(K33( the carrier of c3, the carrier of ()))
n9 is Element of the carrier of c3
X is Element of the carrier of c3
f . n9 is Element of the carrier of ()
f . X is Element of the carrier of ()
n9 is Element of the carrier of c3
f . n9 is Element of the carrier of ()
X is Element of the carrier of c3
f . X is Element of the carrier of ()
{(Top c3)} is non empty trivial V56() 1 -element Element of K32( the carrier of c3)
K32( the carrier of c3) is V56() V60() set
the carrier of c3 \ {(Top c3)} is V56() Element of K32( the carrier of c3)
card ( the carrier of c3 \ {(Top c3)}) is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
card the carrier of c3 is non empty ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
card {(Top c3)} is non empty ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
(card the carrier of c3) - (card {(Top c3)}) is V24() ext-real V32() set
(A + 1) - 1 is V24() ext-real V32() set
1 - 1 is V24() ext-real V32() set
Ab is non empty V56() Element of K32( the carrier of c3)

the carrier of B is V56() set
card the carrier of B is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
the carrier of () is set
K33( the carrier of B, the carrier of ()) is set
K32(K33( the carrier of B, the carrier of ())) is set
f is Relation-like the carrier of B -defined the carrier of () -valued Function-like V29( the carrier of B, the carrier of ()) V56() Element of K32(K33( the carrier of B, the carrier of ()))
succ A is set
{A} is non empty trivial V35() V36() V37() V38() V39() V40() V56() V60() 1 -element set
A \/ {A} is non empty V56() set
the carrier of (InclPoset (A + 1)) is non empty set
K32( the carrier of (InclPoset (A + 1))) is set

n9 is non empty Element of K32( the carrier of (InclPoset (A + 1)))
subrelstr n9 is non empty strict V80() reflexive transitive antisymmetric full SubRelStr of InclPoset (A + 1)
the carrier of () is non empty set
the carrier of (InclPoset {(Top c3)}) is non empty set
K32( the carrier of (InclPoset {(Top c3)})) is set
b9 is non empty Element of K32( the carrier of (InclPoset {(Top c3)}))

the carrier of () is non empty set
the carrier of () --> A is Relation-like the carrier of () -defined {A} -valued Function-like V29( the carrier of (),{A}) Element of K32(K33( the carrier of (),{A}))
K33( the carrier of (),{A}) is set
K32(K33( the carrier of (),{A})) is set
dom ( the carrier of () --> A) is set
A2 is Element of the carrier of (InclPoset (A + 1))
g is Element of the carrier of (InclPoset (A + 1))
{ b1 where b1 is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT : not A <= b1 } is set
e is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
f is set
{ b1 where b1 is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT : not e <= b1 } is set
f1 is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
the carrier of () \/ {A} is non empty set

the carrier of (subrelstr {(Top c3)}) is non empty V56() set
K33( the carrier of (subrelstr {(Top c3)}), the carrier of ()) is set
K32(K33( the carrier of (subrelstr {(Top c3)}), the carrier of ())) is set
g is Relation-like the carrier of () -defined Function-like V28( the carrier of ()) set
g is Relation-like the carrier of (subrelstr {(Top c3)}) -defined the carrier of () -valued Function-like V29( the carrier of (subrelstr {(Top c3)}), the carrier of ()) V56() Element of K32(K33( the carrier of (subrelstr {(Top c3)}), the carrier of ()))
g . (Top c3) is set
rng g is V56() set
e is Element of the carrier of (subrelstr {(Top c3)})
f is Element of the carrier of (subrelstr {(Top c3)})
g . e is Element of the carrier of ()
g . f is Element of the carrier of ()
e1 is Element of the carrier of ()
g . e1 is set
f1 is Element of the carrier of ()
g . f1 is set
A2 is Element of K32( the carrier of (InclPoset (A + 1)))

K33( the carrier of c3, the carrier of (InclPoset (A + 1))) is set
K32(K33( the carrier of c3, the carrier of (InclPoset (A + 1)))) is set

e is Relation-like the carrier of c3 -defined the carrier of (InclPoset (A + 1)) -valued Function-like V29( the carrier of c3, the carrier of (InclPoset (A + 1))) V56() Element of K32(K33( the carrier of c3, the carrier of (InclPoset (A + 1))))

the carrier of A is V56() set
card the carrier of A is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT
the carrier of () is set
K33( the carrier of A, the carrier of ()) is set
K32(K33( the carrier of A, the carrier of ())) is set
the Relation-like the carrier of A -defined the carrier of () -valued Function-like V29( the carrier of A, the carrier of ()) V56() Element of K32(K33( the carrier of A, the carrier of ())) is Relation-like the carrier of A -defined the carrier of () -valued Function-like V29( the carrier of A, the carrier of ()) V56() Element of K32(K33( the carrier of A, the carrier of ()))

the carrier of A is V56() set
card the carrier of A is ordinal natural V24() ext-real non negative V32() V33() V35() V36() V37() V38() V39() V40() V56() cardinal Element of NAT