:: ORDINAL3 semantic presentation

omega is non empty epsilon-transitive epsilon-connected ordinal set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

1 is non empty epsilon-transitive epsilon-connected ordinal natural Element of omega

a is set

succ a is non empty set

{a} is non empty set

a \/ {a} is non empty set

a is set

succ a is non empty set

{a} is non empty set

a \/ {a} is non empty set

b is set

a is epsilon-transitive epsilon-connected ordinal set

succ a is non empty epsilon-transitive epsilon-connected ordinal set

{a} is non empty set

a \/ {a} is non empty set

b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

a is epsilon-transitive epsilon-connected ordinal set

b is set

union b is set

a is set

a is set

On a is set

union (On a) is set

b is set

a is epsilon-transitive epsilon-connected ordinal set

b is set

On b is set

a is set

b is set

a is set

b is set

a is epsilon-transitive epsilon-connected ordinal set

{a} is non empty set

On {a} is set

succ a is non empty epsilon-transitive epsilon-connected ordinal set

a \/ {a} is non empty set

a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

inf a is epsilon-transitive epsilon-connected ordinal set

On a is set

meet (On a) is set

meet a is set

a is epsilon-transitive epsilon-connected ordinal set

{a} is non empty set

inf {a} is epsilon-transitive epsilon-connected ordinal set

On {a} is set

meet (On {a}) is set

meet {a} is set

a is epsilon-transitive epsilon-connected ordinal set

b is set

meet b is set

inf b is epsilon-transitive epsilon-connected ordinal set

On b is set

meet (On b) is set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a \/ b is set

a /\ b is set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a \/ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a /\ b is epsilon-transitive epsilon-connected ordinal set

succ {} is non empty epsilon-transitive epsilon-connected ordinal natural set

{{}} is non empty set

{} \/ {{}} is non empty set

a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a +^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b +^ b is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a +^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b +^ b is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a +^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a +^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a +^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

{} +^ b is epsilon-transitive epsilon-connected ordinal set

a +^ {} is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

succ a is non empty epsilon-transitive epsilon-connected ordinal set

{a} is non empty set

a \/ {a} is non empty set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

a +^ (succ b) is epsilon-transitive epsilon-connected ordinal set

a +^ {} is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

{} +^ a is epsilon-transitive epsilon-connected ordinal set

a +^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

rng b is set

a is epsilon-transitive epsilon-connected ordinal set

x is set

b . x is set

k is epsilon-transitive epsilon-connected ordinal set

b . k is epsilon-transitive epsilon-connected ordinal set

a +^ k is epsilon-transitive epsilon-connected ordinal set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

succ a is non empty epsilon-transitive epsilon-connected ordinal set

{a} is non empty set

a \/ {a} is non empty set

a +^ a is epsilon-transitive epsilon-connected ordinal set

succ (a +^ a) is non empty epsilon-transitive epsilon-connected ordinal set

{(a +^ a)} is non empty set

(a +^ a) \/ {(a +^ a)} is non empty set

a +^ (succ a) is epsilon-transitive epsilon-connected ordinal set

sup b is epsilon-transitive epsilon-connected ordinal set

a +^ {} is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a +^ a is epsilon-transitive epsilon-connected ordinal set

a +^ {} is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a +^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

sup a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

b is epsilon-transitive epsilon-connected ordinal set

b +^ b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

a . (succ b) is epsilon-transitive epsilon-connected ordinal set

b +^ (succ b) is epsilon-transitive epsilon-connected ordinal set

succ (b +^ b) is non empty epsilon-transitive epsilon-connected ordinal set

{(b +^ b)} is non empty set

(b +^ b) \/ {(b +^ b)} is non empty set

(succ b) +^ {} is epsilon-transitive epsilon-connected ordinal set

b +^ {} is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a +^ b) +^ a is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

a +^ (b +^ a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(a +^ b) +^ b is epsilon-transitive epsilon-connected ordinal set

b +^ b is epsilon-transitive epsilon-connected ordinal set

a +^ (b +^ b) is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

(a +^ b) +^ (succ b) is epsilon-transitive epsilon-connected ordinal set

b +^ (succ b) is epsilon-transitive epsilon-connected ordinal set

a +^ (b +^ (succ b)) is epsilon-transitive epsilon-connected ordinal set

succ ((a +^ b) +^ b) is non empty epsilon-transitive epsilon-connected ordinal set

{((a +^ b) +^ b)} is non empty set

((a +^ b) +^ b) \/ {((a +^ b) +^ b)} is non empty set

succ (b +^ b) is non empty epsilon-transitive epsilon-connected ordinal set

{(b +^ b)} is non empty set

(b +^ b) \/ {(b +^ b)} is non empty set

a +^ (succ (b +^ b)) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(a +^ b) +^ b is epsilon-transitive epsilon-connected ordinal set

b +^ b is epsilon-transitive epsilon-connected ordinal set

a +^ (b +^ b) is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

rng b is set

rng a is set

x is set

k is set

b . k is set

m is epsilon-transitive epsilon-connected ordinal set

b +^ m is epsilon-transitive epsilon-connected ordinal set

b . m is epsilon-transitive epsilon-connected ordinal set

(a +^ b) +^ m is epsilon-transitive epsilon-connected ordinal set

a +^ (b +^ m) is epsilon-transitive epsilon-connected ordinal set

a . (b +^ m) is epsilon-transitive epsilon-connected ordinal set

sup a is epsilon-transitive epsilon-connected ordinal set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

sup b is epsilon-transitive epsilon-connected ordinal set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

x is set

k is epsilon-transitive epsilon-connected ordinal set

m is epsilon-transitive epsilon-connected ordinal set

a +^ m is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

b +^ n is epsilon-transitive epsilon-connected ordinal set

a +^ (b +^ n) is epsilon-transitive epsilon-connected ordinal set

(a +^ b) +^ n is epsilon-transitive epsilon-connected ordinal set

(a +^ b) +^ {} is epsilon-transitive epsilon-connected ordinal set

(a +^ b) +^ {} is epsilon-transitive epsilon-connected ordinal set

b +^ {} is epsilon-transitive epsilon-connected ordinal set

a +^ (b +^ {}) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

1 *^ b is epsilon-transitive epsilon-connected ordinal set

b *^ 1 is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

b *^ 1 is epsilon-transitive epsilon-connected ordinal set

1 *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

1 *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b +^ b is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

b is set

a . b is set

a is epsilon-transitive epsilon-connected ordinal set

b . a is epsilon-transitive epsilon-connected ordinal set

a +^ (b . a) is epsilon-transitive epsilon-connected ordinal set

b . b is set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

b is set

a . b is set

a is epsilon-transitive epsilon-connected ordinal set

b . a is epsilon-transitive epsilon-connected ordinal set

(b . a) +^ a is epsilon-transitive epsilon-connected ordinal set

b . b is set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

b is set

a . b is set

a is epsilon-transitive epsilon-connected ordinal set

b . a is epsilon-transitive epsilon-connected ordinal set

a *^ (b . a) is epsilon-transitive epsilon-connected ordinal set

b . b is set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

b is set

a . b is set

a is epsilon-transitive epsilon-connected ordinal set

b . a is epsilon-transitive epsilon-connected ordinal set

(b . a) *^ a is epsilon-transitive epsilon-connected ordinal set

b . b is set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

sup a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

sup b is epsilon-transitive epsilon-connected ordinal set

rng b is set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a +^ (sup a) is epsilon-transitive epsilon-connected ordinal set

the epsilon-transitive epsilon-connected ordinal Element of dom a is epsilon-transitive epsilon-connected ordinal Element of dom a

a . the epsilon-transitive epsilon-connected ordinal Element of dom a is epsilon-transitive epsilon-connected ordinal set

a +^ (sup (rng a)) is epsilon-transitive epsilon-connected ordinal set

a is set

x is epsilon-transitive epsilon-connected ordinal set

k is epsilon-transitive epsilon-connected ordinal set

a +^ k is epsilon-transitive epsilon-connected ordinal set

m is epsilon-transitive epsilon-connected ordinal set

n is set

a . n is set

y9 is epsilon-transitive epsilon-connected ordinal set

b . y9 is epsilon-transitive epsilon-connected ordinal set

a +^ m is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

b . the epsilon-transitive epsilon-connected ordinal Element of dom a is epsilon-transitive epsilon-connected ordinal set

a is set

x is epsilon-transitive epsilon-connected ordinal set

k is epsilon-transitive epsilon-connected ordinal set

m is set

b . m is set

n is epsilon-transitive epsilon-connected ordinal set

a . n is epsilon-transitive epsilon-connected ordinal set

y9 is epsilon-transitive epsilon-connected ordinal set

a +^ y9 is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

sup a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

union (sup a) is epsilon-transitive epsilon-connected ordinal set

union (sup (rng a)) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

b is set

a is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal set

k is set

a . k is set

succ x is non empty epsilon-transitive epsilon-connected ordinal set

{x} is non empty set

x \/ {x} is non empty set

m is epsilon-transitive epsilon-connected ordinal set

succ m is non empty epsilon-transitive epsilon-connected ordinal set

{m} is non empty set

m \/ {m} is non empty set

a . (succ m) is epsilon-transitive epsilon-connected ordinal set

(succ m) *^ b is epsilon-transitive epsilon-connected ordinal set

m *^ b is epsilon-transitive epsilon-connected ordinal set

(m *^ b) +^ b is epsilon-transitive epsilon-connected ordinal set

(m *^ b) +^ (succ {}) is epsilon-transitive epsilon-connected ordinal set

(m *^ b) +^ {} is epsilon-transitive epsilon-connected ordinal set

succ ((m *^ b) +^ {}) is non empty epsilon-transitive epsilon-connected ordinal set

{((m *^ b) +^ {})} is non empty set

((m *^ b) +^ {}) \/ {((m *^ b) +^ {})} is non empty set

a . m is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

sup b is epsilon-transitive epsilon-connected ordinal set

rng b is set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

union (sup b) is epsilon-transitive epsilon-connected ordinal set

union (sup (rng b)) is epsilon-transitive epsilon-connected ordinal set

b is set

a is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal set

k is set

b . k is set

m is epsilon-transitive epsilon-connected ordinal set

succ m is non empty epsilon-transitive epsilon-connected ordinal set

{m} is non empty set

m \/ {m} is non empty set

n is non empty epsilon-transitive epsilon-connected ordinal set

n *^ a is epsilon-transitive epsilon-connected ordinal set

x +^ {} is epsilon-transitive epsilon-connected ordinal set

m *^ a is epsilon-transitive epsilon-connected ordinal set

(m *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set

x +^ a is epsilon-transitive epsilon-connected ordinal set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

sup a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

sup b is epsilon-transitive epsilon-connected ordinal set

rng b is set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(sup a) *^ a is epsilon-transitive epsilon-connected ordinal set

(sup (rng a)) *^ a is epsilon-transitive epsilon-connected ordinal set

b is set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ a is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal set

k is set

a . k is set

m is epsilon-transitive epsilon-connected ordinal set

b . m is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

x *^ a is epsilon-transitive epsilon-connected ordinal set

b is set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

x is set

b . x is set

k is epsilon-transitive epsilon-connected ordinal set

a . k is epsilon-transitive epsilon-connected ordinal set

m is epsilon-transitive epsilon-connected ordinal set

m *^ a is epsilon-transitive epsilon-connected ordinal set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

sup a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(b,a) is T-Sequence-like Relation-like Function-like Ordinal-yielding set

sup (b,a) is epsilon-transitive epsilon-connected ordinal set

rng (b,a) is set

sup (rng (b,a)) is epsilon-transitive epsilon-connected ordinal set

b +^ (sup a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a . a is epsilon-transitive epsilon-connected ordinal set

(b,a) . a is epsilon-transitive epsilon-connected ordinal set

b +^ b is epsilon-transitive epsilon-connected ordinal set

dom (b,a) is epsilon-transitive epsilon-connected ordinal set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

sup a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(b,a) is T-Sequence-like Relation-like Function-like Ordinal-yielding set

sup (b,a) is epsilon-transitive epsilon-connected ordinal set

rng (b,a) is set

sup (rng (b,a)) is epsilon-transitive epsilon-connected ordinal set

(sup a) *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a . a is epsilon-transitive epsilon-connected ordinal set

(b,a) . a is epsilon-transitive epsilon-connected ordinal set

b *^ b is epsilon-transitive epsilon-connected ordinal set

dom (b,a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

union a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

union (b +^ a) is epsilon-transitive epsilon-connected ordinal set

b +^ (union a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

succ a is non empty epsilon-transitive epsilon-connected ordinal set

{a} is non empty set

a \/ {a} is non empty set

b +^ a is epsilon-transitive epsilon-connected ordinal set

succ (b +^ a) is non empty epsilon-transitive epsilon-connected ordinal set

{(b +^ a)} is non empty set

(b +^ a) \/ {(b +^ a)} is non empty set

union (succ (b +^ a)) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

succ a is non empty epsilon-transitive epsilon-connected ordinal set

{a} is non empty set

a \/ {a} is non empty set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a +^ b) *^ a is epsilon-transitive epsilon-connected ordinal set

a *^ a is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

(a +^ b) *^ a is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

a +^ (succ b) is epsilon-transitive epsilon-connected ordinal set

(a +^ (succ b)) *^ a is epsilon-transitive epsilon-connected ordinal set

(succ b) *^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ ((succ b) *^ a) is epsilon-transitive epsilon-connected ordinal set

succ (a +^ b) is non empty epsilon-transitive epsilon-connected ordinal set

{(a +^ b)} is non empty set

(a +^ b) \/ {(a +^ b)} is non empty set

(succ (a +^ b)) *^ a is epsilon-transitive epsilon-connected ordinal set

((a *^ a) +^ (b *^ a)) +^ a is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ ((b *^ a) +^ a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

(a +^ b) *^ a is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

(a,b) is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom (a,b) is epsilon-transitive epsilon-connected ordinal set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

x is set

k is epsilon-transitive epsilon-connected ordinal set

b . k is epsilon-transitive epsilon-connected ordinal set

a . k is epsilon-transitive epsilon-connected ordinal set

(a,b) . x is set

m is epsilon-transitive epsilon-connected ordinal set

m *^ a is epsilon-transitive epsilon-connected ordinal set

a +^ k is epsilon-transitive epsilon-connected ordinal set

(a +^ k) *^ a is epsilon-transitive epsilon-connected ordinal set

k *^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ (k *^ a) is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ n is epsilon-transitive epsilon-connected ordinal set

((a *^ a),a) is T-Sequence-like Relation-like Function-like Ordinal-yielding set

((a *^ a),a) . x is set

a . {} is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

dom ((a *^ a),a) is epsilon-transitive epsilon-connected ordinal set

sup b is epsilon-transitive epsilon-connected ordinal set

rng b is set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

sup (a,b) is epsilon-transitive epsilon-connected ordinal set

rng (a,b) is set

sup (rng (a,b)) is epsilon-transitive epsilon-connected ordinal set

sup a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ (sup a) is epsilon-transitive epsilon-connected ordinal set

union ((a *^ a) +^ (sup a)) is epsilon-transitive epsilon-connected ordinal set

union (sup a) is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ (union (sup a)) is epsilon-transitive epsilon-connected ordinal set

a +^ {} is epsilon-transitive epsilon-connected ordinal set

(a +^ {}) *^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ {} is epsilon-transitive epsilon-connected ordinal set

{} *^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ ({} *^ a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ 1 is epsilon-transitive epsilon-connected ordinal set

a *^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

b *^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ {} is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

succ a is non empty epsilon-transitive epsilon-connected ordinal set

{a} is non empty set

a \/ {a} is non empty set

b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

a is non empty epsilon-transitive epsilon-connected ordinal set

a *^ a is epsilon-transitive epsilon-connected ordinal set

x is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

(a *^ a) +^ x is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ a is epsilon-transitive epsilon-connected ordinal set

x is non empty epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ x is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ a is epsilon-transitive epsilon-connected ordinal set

x is non empty epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ x is epsilon-transitive epsilon-connected ordinal set

k is non empty epsilon-transitive epsilon-connected ordinal set

k *^ a is epsilon-transitive epsilon-connected ordinal set

m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

(k *^ a) +^ m is epsilon-transitive epsilon-connected ordinal set

a is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

a *^ a is epsilon-transitive epsilon-connected ordinal set

b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

(a *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

{} +^ {} is epsilon-transitive epsilon-connected ordinal natural set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal set

b +^ x is epsilon-transitive epsilon-connected ordinal set

x *^ a is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ (x *^ a) is epsilon-transitive epsilon-connected ordinal set

((b *^ a) +^ (x *^ a)) +^ a is epsilon-transitive epsilon-connected ordinal set

(x *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ ((x *^ a) +^ a) is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal set

b +^ x is epsilon-transitive epsilon-connected ordinal set

x *^ a is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ (x *^ a) is epsilon-transitive epsilon-connected ordinal set

((b *^ a) +^ (x *^ a)) +^ b is epsilon-transitive epsilon-connected ordinal set

(x *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ ((x *^ a) +^ b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

a is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

sup a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

a is set

a . a is set

x is epsilon-transitive epsilon-connected ordinal set

x *^ a is epsilon-transitive epsilon-connected ordinal set

b +^ 1 is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

succ x is non empty epsilon-transitive epsilon-connected ordinal set

{x} is non empty set

x \/ {x} is non empty set

(succ x) *^ a is epsilon-transitive epsilon-connected ordinal set

(x *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set

a . (succ x) is epsilon-transitive epsilon-connected ordinal set

union (sup a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

a *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

{} *^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ b is epsilon-transitive epsilon-connected ordinal set

(b *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set

b *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

(succ b) *^ b is epsilon-transitive epsilon-connected ordinal set

((succ b) *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set

(succ b) *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

(b *^ b) +^ b is epsilon-transitive epsilon-connected ordinal set

((b *^ b) +^ b) *^ a is epsilon-transitive epsilon-connected ordinal set

(b *^ (b *^ a)) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

1 *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

(b *^ (b *^ a)) +^ (1 *^ (b *^ a)) is epsilon-transitive epsilon-connected ordinal set

b +^ 1 is epsilon-transitive epsilon-connected ordinal set

(b +^ 1) *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ b is epsilon-transitive epsilon-connected ordinal set

(b *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set

b *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

(a,b) is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom (a,b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a,b) . a is epsilon-transitive epsilon-connected ordinal set

a *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

b . a is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

(b . a) *^ a is epsilon-transitive epsilon-connected ordinal set

1 *^ 1 is epsilon-transitive epsilon-connected ordinal set

sup (a,b) is epsilon-transitive epsilon-connected ordinal set

rng (a,b) is set

sup (rng (a,b)) is epsilon-transitive epsilon-connected ordinal set

sup b is epsilon-transitive epsilon-connected ordinal set

rng b is set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

(b *^ b) *^ 1 is epsilon-transitive epsilon-connected ordinal set

(b *^ b) *^ {} is epsilon-transitive epsilon-connected ordinal set

b *^ 1 is epsilon-transitive epsilon-connected ordinal set

b *^ {} is epsilon-transitive epsilon-connected ordinal set

{} *^ b is epsilon-transitive epsilon-connected ordinal set

({} *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set

{} *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b +^ b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(a *^ b) +^ b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(b *^ b) +^ a is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal set

k is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(a,b) is epsilon-transitive epsilon-connected ordinal set

(a,b) *^ b is epsilon-transitive epsilon-connected ordinal set

(a,((a,b) *^ b)) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(b,a) is epsilon-transitive epsilon-connected ordinal set

a +^ (b,a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

((a +^ b),a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

(b,a) is epsilon-transitive epsilon-connected ordinal set

a +^ (b,a) is epsilon-transitive epsilon-connected ordinal set

a +^ (a,a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

a +^ {} is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(b,a) is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a,{}) is epsilon-transitive epsilon-connected ordinal set

({},a) is epsilon-transitive epsilon-connected ordinal set

{} +^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(a,b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b +^ a is epsilon-transitive epsilon-connected ordinal set

(a,(b +^ a)) is epsilon-transitive epsilon-connected ordinal set

((a,b),a) is epsilon-transitive epsilon-connected ordinal set

(b +^ a) +^ (a,(b +^ a)) is epsilon-transitive epsilon-connected ordinal set

a +^ (a,(b +^ a)) is epsilon-transitive epsilon-connected ordinal set

b +^ (a +^ (a,(b +^ a))) is epsilon-transitive epsilon-connected ordinal set

b +^ (a,b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a,b) is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

(b,a) is epsilon-transitive epsilon-connected ordinal set

a +^ (b,a) is epsilon-transitive epsilon-connected ordinal set

b +^ (a,b) is epsilon-transitive epsilon-connected ordinal set

a +^ (a,a) is epsilon-transitive epsilon-connected ordinal set

(b,a) +^ (a,b) is epsilon-transitive epsilon-connected ordinal set

a +^ ((b,a) +^ (a,b)) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

(b,a) is epsilon-transitive epsilon-connected ordinal set

a +^ (a,a) is epsilon-transitive epsilon-connected ordinal set

a +^ (b,a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a +^ a is epsilon-transitive epsilon-connected ordinal set

(b,a) is epsilon-transitive epsilon-connected ordinal set

((a +^ a),a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

((a +^ b),a) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(a,b) is epsilon-transitive epsilon-connected ordinal set

b +^ (a,b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

((a *^ b),(a *^ b)) is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

(a,a) *^ b is epsilon-transitive epsilon-connected ordinal set

{} *^ b is epsilon-transitive epsilon-connected ordinal set

a *^ {} is epsilon-transitive epsilon-connected ordinal set

a +^ (a,a) is epsilon-transitive epsilon-connected ordinal set

(a *^ b) +^ ((a,a) *^ b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(a,b) is epsilon-transitive epsilon-connected ordinal set

(a,b) *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

((a,b) *^ b) +^ a is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(a,b) is epsilon-transitive epsilon-connected ordinal set

(a,b) *^ b is epsilon-transitive epsilon-connected ordinal set

(a,b) is epsilon-transitive epsilon-connected ordinal set

(a,((a,b) *^ b)) is epsilon-transitive epsilon-connected ordinal set

((a,b) *^ b) +^ (a,b) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

(a,a) *^ a is epsilon-transitive epsilon-connected ordinal set

(a,((a,a) *^ a)) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

(a,a) *^ a is epsilon-transitive epsilon-connected ordinal set

(a,((a,a) *^ a)) is epsilon-transitive epsilon-connected ordinal set

((a,a) *^ a) +^ (a,a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

((a,a) *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

((a,a) *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ a is epsilon-transitive epsilon-connected ordinal set

((b *^ a),a) is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ {} is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

((a *^ b),b) is epsilon-transitive epsilon-connected ordinal set

((a *^ b),b) is epsilon-transitive epsilon-connected ordinal set

((a *^ b),b) *^ b is epsilon-transitive epsilon-connected ordinal set

((a *^ b),(((a *^ b),b) *^ b)) is epsilon-transitive epsilon-connected ordinal set

a *^ {} is epsilon-transitive epsilon-connected ordinal set

((a *^ b),(a *^ b)) is epsilon-transitive epsilon-connected ordinal set

({},(((a *^ b),b) *^ b)) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

({},a) is epsilon-transitive epsilon-connected ordinal set

({},a) is epsilon-transitive epsilon-connected ordinal set

({},a) *^ a is epsilon-transitive epsilon-connected ordinal set

({},(({},a) *^ a)) is epsilon-transitive epsilon-connected ordinal set

(a,{}) is epsilon-transitive epsilon-connected ordinal set

(a,{}) is epsilon-transitive epsilon-connected ordinal set

(a,{}) *^ {} is epsilon-transitive epsilon-connected ordinal set

(a,((a,{}) *^ {})) is epsilon-transitive epsilon-connected ordinal set

{} *^ a is epsilon-transitive epsilon-connected ordinal set

(a,{}) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(a,1) is epsilon-transitive epsilon-connected ordinal set

(a,1) is epsilon-transitive epsilon-connected ordinal set

(a,1) *^ 1 is epsilon-transitive epsilon-connected ordinal set

(a,((a,1) *^ 1)) is epsilon-transitive epsilon-connected ordinal set

a *^ 1 is epsilon-transitive epsilon-connected ordinal set

a +^ {} is epsilon-transitive epsilon-connected ordinal set

(a,a) is epsilon-transitive epsilon-connected ordinal set

a is set

sup a is epsilon-transitive epsilon-connected ordinal set

On a is set

union (On a) is set

succ (union (On a)) is non empty set

{(union (On a))} is non empty set

(union (On a)) \/ {(union (On a))} is non empty set

b is epsilon-transitive epsilon-connected ordinal set

succ b is non empty epsilon-transitive epsilon-connected ordinal set

{b} is non empty set

b \/ {b} is non empty set

a is set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

succ a is non empty epsilon-transitive epsilon-connected ordinal set

{a} is non empty set

a \/ {a} is non empty set

b is T-Sequence-like Relation-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

rng b is set

sup b is epsilon-transitive epsilon-connected ordinal set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

a is set

b is set

b . b is set

b is epsilon-transitive epsilon-connected ordinal set

b . b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b . a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b . b is epsilon-transitive epsilon-connected ordinal set

b . {} is epsilon-transitive epsilon-connected ordinal set

{(b . {})} is non empty set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a +^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal natural set

b is epsilon-transitive epsilon-connected ordinal natural set

(a,b) is epsilon-transitive epsilon-connected ordinal set

b +^ (a,b) is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal natural set

a *^ b is epsilon-transitive epsilon-connected ordinal set

succ a is non empty epsilon-transitive epsilon-connected ordinal natural set

{a} is non empty set

a \/ {a} is non empty set

(succ a) *^ b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal natural set

b +^ b is epsilon-transitive epsilon-connected ordinal natural set

{} *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a *^ b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal natural set

b is epsilon-transitive epsilon-connected ordinal natural set

a +^ b is epsilon-transitive epsilon-connected ordinal natural set

b +^ a is epsilon-transitive epsilon-connected ordinal natural set

b is epsilon-transitive epsilon-connected ordinal natural set

a +^ b is epsilon-transitive epsilon-connected ordinal natural set

b +^ a is epsilon-transitive epsilon-connected ordinal natural set

succ b is non empty epsilon-transitive epsilon-connected ordinal natural set

{b} is non empty set

b \/ {b} is non empty set

a is epsilon-transitive epsilon-connected ordinal natural set

(succ b) +^ a is epsilon-transitive epsilon-connected ordinal natural set

b +^ a is epsilon-transitive epsilon-connected ordinal natural set

succ (b +^ a) is non empty epsilon-transitive epsilon-connected ordinal natural set

{(b +^ a)} is non empty set

(b +^ a) \/ {(b +^ a)} is non empty set

succ a is non empty epsilon-transitive epsilon-connected ordinal natural set

{a} is non empty set

a \/ {a} is non empty set

(succ b) +^ (succ a) is epsilon-transitive epsilon-connected ordinal natural set

succ ((succ b) +^ a) is non empty epsilon-transitive epsilon-connected ordinal natural set

{((succ b) +^ a)} is non empty set

((succ b) +^ a) \/ {((succ b) +^ a)} is non empty set

b +^ (succ a) is epsilon-transitive epsilon-connected ordinal natural set

succ (b +^ (succ a)) is non empty epsilon-transitive epsilon-connected ordinal natural set

{(b +^ (succ a))} is non empty set

(b +^ (succ a)) \/ {(b +^ (succ a))} is non empty set

(succ b) +^ {} is epsilon-transitive epsilon-connected ordinal natural set

b +^ {} is epsilon-transitive epsilon-connected ordinal natural set

succ (b +^ {}) is non empty epsilon-transitive epsilon-connected ordinal natural set

{(b +^ {})} is non empty set

(b +^ {}) \/ {(b +^ {})} is non empty set

(succ b) +^ a is epsilon-transitive epsilon-connected ordinal natural set

succ (b +^ a) is non empty epsilon-transitive epsilon-connected ordinal natural set

{(b +^ a)} is non empty set

(b +^ a) \/ {(b +^ a)} is non empty set

a +^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set

a +^ {} is epsilon-transitive epsilon-connected ordinal natural set

{} +^ a is epsilon-transitive epsilon-connected ordinal natural set

a is epsilon-transitive epsilon-connected ordinal natural set

b is epsilon-transitive epsilon-connected ordinal natural set

a *^ b is epsilon-transitive epsilon-connected ordinal natural set

b *^ a is epsilon-transitive epsilon-connected ordinal natural set

b is epsilon-transitive epsilon-connected ordinal natural set

succ b is non empty epsilon-transitive epsilon-connected ordinal natural set

{b} is non empty set

b \/ {b} is non empty set

a *^ b is epsilon-transitive epsilon-connected ordinal natural set

b *^ a is epsilon-transitive epsilon-connected ordinal natural set

a is epsilon-transitive epsilon-connected ordinal natural set

a *^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set

a *^ b is epsilon-transitive epsilon-connected ordinal natural set

((a *^ b),a) is epsilon-transitive epsilon-connected ordinal natural set

succ a is non empty epsilon-transitive epsilon-connected ordinal natural set

{a} is non empty set

a \/ {a} is non empty set

(succ a) *^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set

((a *^ (succ b)),(succ b)) is epsilon-transitive epsilon-connected ordinal natural set

(a,(succ b)) is epsilon-transitive epsilon-connected ordinal natural set

((a *^ b),(a,(succ b))) is epsilon-transitive epsilon-connected ordinal natural set

(a,b) is epsilon-transitive epsilon-connected ordinal natural set

succ (a,b) is non empty epsilon-transitive epsilon-connected ordinal natural set

{(a,b)} is non empty set

(a,b) \/ {(a,b)} is non empty set

((a *^ b),(succ (a,b))) is epsilon-transitive epsilon-connected ordinal natural set

((a *^ b),(a,b)) is epsilon-transitive epsilon-connected ordinal natural set

succ ((a *^ b),(a,b)) is non empty epsilon-transitive epsilon-connected ordinal natural set

{((a *^ b),(a,b))} is non empty set

((a *^ b),(a,b)) \/ {((a *^ b),(a,b))} is non empty set

((a *^ b),b) is epsilon-transitive epsilon-connected ordinal natural set

(((a *^ b),b),a) is epsilon-transitive epsilon-connected ordinal natural set

succ (((a *^ b),b),a) is non empty epsilon-transitive epsilon-connected ordinal natural set

{(((a *^ b),b),a)} is non empty set

(((a *^ b),b),a) \/ {(((a *^ b),b),a)} is non empty set

(succ a) *^ b is epsilon-transitive epsilon-connected ordinal natural set

(((succ a) *^ b),a) is epsilon-transitive epsilon-connected ordinal natural set

succ (((succ a) *^ b),a) is non empty epsilon-transitive epsilon-connected ordinal natural set

{(((succ a) *^ b),a)} is non empty set

(((succ a) *^ b),a) \/ {(((succ a) *^ b),a)} is non empty set

(((succ a) *^ b),(succ a)) is epsilon-transitive epsilon-connected ordinal natural set

{} *^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set

({},{}) is epsilon-transitive epsilon-connected ordinal natural set

{} *^ b is epsilon-transitive epsilon-connected ordinal natural set

(({} *^ b),{}) is epsilon-transitive epsilon-connected ordinal natural set

a *^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set

((a *^ b),a) is epsilon-transitive epsilon-connected ordinal natural set

(succ b) *^ a is epsilon-transitive epsilon-connected ordinal natural set

a *^ {} is epsilon-transitive epsilon-connected ordinal natural set

{} *^ a is epsilon-transitive epsilon-connected ordinal natural set