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

the empty trivial finite {} -element RelStr is empty trivial finite {} -element RelStr

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

c

b is set

[f,c

{f,c

{f} is non empty trivial V56() 1 -element set

{{f,c

[c

{c

{c

{{c

[f,b] is set

{f,b} is non empty V56() set

{{f,b},{f}} is non empty V56() V60() set

f is set

c

[f,c

{f,c

{f} is non empty trivial V56() 1 -element set

{{f,c

[c

{c

{c

{{c

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

the non empty trivial finite 1 -element V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() distributive complemented RelStr is non empty trivial finite 1 -element V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() distributive complemented RelStr

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

the non empty trivial finite 1 -element V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() distributive complemented RelStr is non empty trivial finite 1 -element V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() connected V204() V205() distributive complemented RelStr

the finite V80() reflexive transitive antisymmetric () is finite 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

c

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

A is ordinal natural V24() ext-real non negative V32() V56() cardinal set

f is ordinal natural V24() ext-real non negative V32() V56() cardinal set

InclPoset A is strict V80() reflexive transitive antisymmetric RelStr

InclPoset f is strict V80() reflexive transitive antisymmetric RelStr

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

the carrier of (InclPoset f) is set

K33( the carrier of (InclPoset f), the carrier of (InclPoset f)) is set

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

RelIncl f is Relation-like f -defined f -valued V28(f) reflexive antisymmetric transitive V56() Element of K32(K33(f,f))

K33(f,f) is V56() set

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

RelIncl A is Relation-like A -defined A -valued V28(A) reflexive antisymmetric transitive V56() Element of K32(K33(A,A))

K33(A,A) is V56() set

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

c

(RelIncl f) |_2 A is Relation-like set

(RelIncl f) /\ K33(A,A) is V56() set

the carrier of (InclPoset A) is set

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

K33( the carrier of (InclPoset A), the carrier of (InclPoset A)) is set

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

(RelIncl f) |_2 A is Relation-like set

(RelIncl f) /\ K33(A,A) is V56() set

the InternalRel of (InclPoset f) |_2 the carrier of (InclPoset A) is Relation-like set

the InternalRel of (InclPoset f) /\ K33( the carrier of (InclPoset A), the carrier of (InclPoset A)) is set

A is RelStr

f is set

c

f /\ c

b is set

f \/ c

the carrier of A is set

Ab is Element of the carrier of A

A is non empty antisymmetric upper-bounded RelStr

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

c

( 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

c

A is antisymmetric RelStr

the carrier of A is set

K32( the carrier of A) is set

f is antisymmetric RelStr

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

c

b is Element of K32( the carrier of A)

subrelstr c

the carrier of (subrelstr c

subrelstr b is strict antisymmetric full SubRelStr of A

the carrier of (subrelstr b) is set

c

Ab is Element of K32( the carrier of f)

B is Element of K32( the carrier of f)

subrelstr Ab is strict antisymmetric full SubRelStr of f

the carrier of (subrelstr Ab) is set

K33( the carrier of (subrelstr c

K32(K33( the carrier of (subrelstr c

subrelstr B is strict antisymmetric full SubRelStr of f

the carrier of (subrelstr B) is set

K33( the carrier of (subrelstr b), the carrier of (subrelstr B)) is set

K32(K33( the carrier of (subrelstr b), the carrier of (subrelstr B))) is set

Ab \/ B is Element of K32( the carrier of f)

f is Relation-like the carrier of (subrelstr c

n9 is Relation-like the carrier of (subrelstr b) -defined the carrier of (subrelstr B) -valued Function-like V29( the carrier of (subrelstr b), the carrier of (subrelstr B)) Element of K32(K33( the carrier of (subrelstr b), the carrier of (subrelstr B)))

f +* n9 is Relation-like Function-like set

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 (subrelstr e) 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 (subrelstr g) is non empty set

K33( the carrier of (subrelstr e), the carrier of (subrelstr g)) is set

K32(K33( the carrier of (subrelstr e), the carrier of (subrelstr g))) is set

f . g is set

f . A2 is set

f is Element of the carrier of (subrelstr e)

f1 is Element of the carrier of (subrelstr e)

e1 is Relation-like the carrier of (subrelstr e) -defined the carrier of (subrelstr g) -valued Function-like V29( the carrier of (subrelstr e), the carrier of (subrelstr g)) Element of K32(K33( the carrier of (subrelstr e), the carrier of (subrelstr g)))

e1 . f is Element of the carrier of (subrelstr g)

e1 . f1 is Element of the carrier of (subrelstr g)

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 (subrelstr f) 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 (subrelstr g) is non empty set

K33( the carrier of (subrelstr f), the carrier of (subrelstr g)) is set

K32(K33( the carrier of (subrelstr f), the carrier of (subrelstr g))) 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 (subrelstr f1) 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 (subrelstr e) is non empty set

K33( the carrier of (subrelstr f1), the carrier of (subrelstr e)) is set

K32(K33( the carrier of (subrelstr f1), the carrier of (subrelstr e))) is set

e1 is Relation-like the carrier of (subrelstr f) -defined the carrier of (subrelstr g) -valued Function-like V29( the carrier of (subrelstr f), the carrier of (subrelstr g)) Element of K32(K33( the carrier of (subrelstr f), the carrier of (subrelstr g)))

ax is Element of the carrier of (subrelstr f)

e1 . ax is Element of the carrier of (subrelstr g)

g9 is Relation-like the carrier of (subrelstr f1) -defined the carrier of (subrelstr e) -valued Function-like V29( the carrier of (subrelstr f1), the carrier of (subrelstr e)) Element of K32(K33( the carrier of (subrelstr f1), the carrier of (subrelstr e)))

ay is Element of the carrier of (subrelstr f1)

g9 . ay is Element of the carrier of (subrelstr e)

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 (subrelstr e) 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 (subrelstr g) is non empty set

K33( the carrier of (subrelstr e), the carrier of (subrelstr g)) is set

K32(K33( the carrier of (subrelstr e), the carrier of (subrelstr g))) is set

n9 . g is set

n9 . A2 is set

f is Element of the carrier of (subrelstr e)

f1 is Element of the carrier of (subrelstr e)

e1 is Relation-like the carrier of (subrelstr e) -defined the carrier of (subrelstr g) -valued Function-like V29( the carrier of (subrelstr e), the carrier of (subrelstr g)) Element of K32(K33( the carrier of (subrelstr e), the carrier of (subrelstr g)))

e1 . f is Element of the carrier of (subrelstr g)

e1 . f1 is Element of the carrier of (subrelstr g)

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 is ordinal natural V24() ext-real non negative V32() V56() cardinal set

InclPoset A is strict V80() reflexive transitive antisymmetric RelStr

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

f is finite V80() reflexive transitive antisymmetric ()

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

c

Top c

the carrier of c

Ab is set

{Ab} is non empty trivial V56() 1 -element set

InclPoset 1 is non empty strict V80() reflexive transitive antisymmetric RelStr

the carrier of c

{0} is non empty trivial V35() V36() V37() V38() V39() V40() V56() V60() 1 -element set

K33( the carrier of c

K32(K33( the carrier of c

rng ( the carrier of c

the carrier of (InclPoset 1) is non empty set

K33( the carrier of c

K32(K33( the carrier of c

f is Relation-like the carrier of c

n9 is Element of the carrier of c

X is Element of the carrier of c

f . n9 is Element of the carrier of (InclPoset 1)

f . X is Element of the carrier of (InclPoset 1)

n9 is Element of the carrier of c

f . n9 is Element of the carrier of (InclPoset 1)

X is Element of the carrier of c

f . X is Element of the carrier of (InclPoset 1)

{(Top c

K32( the carrier of c

the carrier of c

card ( the carrier of c

card the carrier of c

card {(Top c

(card the carrier of c

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

subrelstr Ab is non empty finite strict V80() reflexive transitive antisymmetric V110() V111() V112() lower-bounded upper-bounded V175() full connected V204() V205() SubRelStr of c

B is finite V80() reflexive transitive antisymmetric ()

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 (InclPoset A) is set

K33( the carrier of B, the carrier of (InclPoset A)) is set

K32(K33( the carrier of B, the carrier of (InclPoset A))) is set

f is Relation-like the carrier of B -defined the carrier of (InclPoset A) -valued Function-like V29( the carrier of B, the carrier of (InclPoset A)) V56() Element of K32(K33( the carrier of B, the carrier of (InclPoset A)))

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

InclPoset {(Top c

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 (subrelstr n9) is non empty set

the carrier of (InclPoset {(Top c

K32( the carrier of (InclPoset {(Top c

b9 is non empty Element of K32( the carrier of (InclPoset {(Top c

subrelstr b9 is non empty strict V80() reflexive transitive antisymmetric full SubRelStr of InclPoset {(Top c

the carrier of (subrelstr b9) is non empty set

the carrier of (subrelstr b9) --> A is Relation-like the carrier of (subrelstr b9) -defined {A} -valued Function-like V29( the carrier of (subrelstr b9),{A}) Element of K32(K33( the carrier of (subrelstr b9),{A}))

K33( the carrier of (subrelstr b9),{A}) is set

K32(K33( the carrier of (subrelstr b9),{A})) is set

dom ( the carrier of (subrelstr b9) --> A) is set

A2 is Element of the carrier of (InclPoset (A + 1))

g is Element of the carrier of (InclPoset (A + 1))

{ b

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

{ b

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 (InclPoset A) \/ {A} is non empty set

subrelstr {(Top c

the carrier of (subrelstr {(Top c

K33( the carrier of (subrelstr {(Top c

K32(K33( the carrier of (subrelstr {(Top c

g is Relation-like the carrier of (subrelstr b9) -defined Function-like V28( the carrier of (subrelstr b9)) set

g is Relation-like the carrier of (subrelstr {(Top c

g . (Top c

rng g is V56() set

e is Element of the carrier of (subrelstr {(Top c

f is Element of the carrier of (subrelstr {(Top c

g . e is Element of the carrier of (subrelstr n9)

g . f is Element of the carrier of (subrelstr n9)

e1 is Element of the carrier of (subrelstr b9)

g . e1 is set

f1 is Element of the carrier of (subrelstr b9)

g . f1 is set

A2 is Element of K32( the carrier of (InclPoset (A + 1)))

subrelstr A2 is strict V80() reflexive transitive antisymmetric full SubRelStr of InclPoset (A + 1)

K33( the carrier of c

K32(K33( the carrier of c

f +* g is Relation-like Function-like V56() set

e is Relation-like the carrier of c

InclPoset 0 is strict V80() reflexive transitive antisymmetric RelStr

A is finite V80() reflexive transitive antisymmetric ()

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 (InclPoset 0) is set

K33( the carrier of A, the carrier of (InclPoset 0)) is set

K32(K33( the carrier of A, the carrier of (InclPoset 0))) is set

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

A is finite V80() reflexive transitive antisymmetric ()

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

f is ordinal natural V24() ext-real non negative V32() V56() cardinal set

InclPoset f is strict V80() reflexive transitive antisymmetric RelStr