:: ORDINAL5 semantic presentation

REAL is set

NAT is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V33() V34() Element of K19(REAL)

K19(REAL) is set

COMPLEX is set

NAT is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V33() V34() set

K19(NAT) is non empty V12() non finite set

K19(NAT) is non empty V12() non finite set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set

the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() Element of NAT

{{}} is functional non empty V12() finite finite-membered V35(1) set

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 Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set

rng a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V12() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V49() V53() set

the set is set

<% the set %> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) V53() set

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

A is Relation-like Function-like non empty T-Sequence-like set

a ^ A is Relation-like Function-like T-Sequence-like set

dom a is epsilon-transitive epsilon-connected ordinal set

dom A is non empty epsilon-transitive epsilon-connected ordinal set

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

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

A ^ a is Relation-like Function-like T-Sequence-like set

dom A is non empty epsilon-transitive epsilon-connected ordinal set

dom a is epsilon-transitive epsilon-connected ordinal set

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

dom (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 +^ A is epsilon-transitive epsilon-connected ordinal set

c

dom c

c

rng c

dom (c

s is Relation-like Function-like T-Sequence-like set

dom s is epsilon-transitive epsilon-connected ordinal set

(c

dom ((c

A is set

B is epsilon-transitive epsilon-connected ordinal set

c

(c

((c

B is epsilon-transitive epsilon-connected ordinal set

c

a +^ c

c

a +^ c

c

s . c

((c

B is epsilon-transitive epsilon-connected ordinal set

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

rng a is set

A is Relation-like Function-like T-Sequence-like set

a ^ A is Relation-like Function-like T-Sequence-like set

rng (a ^ A) is set

rng A is set

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

dom a is epsilon-transitive epsilon-connected ordinal set

dom A is epsilon-transitive epsilon-connected ordinal set

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

b is set

s is set

a . s is set

c is epsilon-transitive epsilon-connected ordinal set

(a ^ A) . c is set

b is set

s is set

A . s is set

c is epsilon-transitive epsilon-connected ordinal set

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

(a ^ A) . ((dom a) +^ c) is set

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

A is Relation-like Function-like T-Sequence-like set

a ^ A is Relation-like Function-like T-Sequence-like set

rng (a ^ A) is set

c

rng a is set

rng A is set

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

dom 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

c

a . c

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

dom 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

c

a . c

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

dom a is epsilon-transitive epsilon-connected ordinal set

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

dom a is epsilon-transitive epsilon-connected ordinal set

a .: NAT is set

a . 0 is set

c

b is set

a . b is set

s is epsilon-transitive epsilon-connected ordinal set

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

a . (succ s) is set

a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set

A is epsilon-transitive epsilon-connected ordinal set

dom a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set

a . A is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set

c

a . c

A is epsilon-transitive epsilon-connected ordinal set

dom a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set

a . A is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set

c

a . c

a is epsilon-transitive epsilon-connected ordinal set

<%a%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) V53() set

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

rng <%a%> is non empty V12() finite V35(1) set

A is set

{a} is non empty V12() finite V35(1) set

a is epsilon-transitive epsilon-connected ordinal set

<%a%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding V53() set

dom <%a%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative Element of K19(NAT)

<%a%> . 0 is epsilon-transitive epsilon-connected ordinal set

c

b is epsilon-transitive epsilon-connected ordinal set

<%a%> . b is epsilon-transitive epsilon-connected ordinal set

<%a%> . c

c

dom <%a%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative set

<%a%> . c

b is epsilon-transitive epsilon-connected ordinal set

<%a%> . b is epsilon-transitive epsilon-connected ordinal set

the epsilon-transitive epsilon-connected ordinal set is epsilon-transitive epsilon-connected ordinal set

<% the epsilon-transitive epsilon-connected ordinal set %> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set

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

dom a is epsilon-transitive epsilon-connected ordinal set

Union a is epsilon-transitive epsilon-connected ordinal set

rng a is set

union (rng a) is set

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

c

a . c

c

b is epsilon-transitive epsilon-connected ordinal set

s is set

a . s is set

c 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 . c is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

A is epsilon-transitive epsilon-connected ordinal set

exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set

c

c

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

exp (NAT,(succ a)) is epsilon-transitive epsilon-connected ordinal set

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

a is epsilon-transitive epsilon-connected ordinal set

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

dom A is epsilon-transitive epsilon-connected ordinal set

c

A . c

b is epsilon-transitive epsilon-connected ordinal set

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

exp (a,c

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

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

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

c

exp (a,c

succ c

exp (a,(succ c

a *^ (exp (a,c

c

exp (a,c

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

dom b is epsilon-transitive epsilon-connected ordinal set

lim b is epsilon-transitive epsilon-connected ordinal set

Union b is epsilon-transitive epsilon-connected ordinal set

rng b is set

union (rng b) is set

s is epsilon-transitive epsilon-connected ordinal set

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

c is set

b . c is set

A is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

exp (a,(succ A)) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

dom A is epsilon-transitive epsilon-connected ordinal set

c

A . c

b is epsilon-transitive epsilon-connected ordinal set

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

exp (a,c

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

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

c

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

dom b is epsilon-transitive epsilon-connected ordinal set

Union b is epsilon-transitive epsilon-connected ordinal set

rng b is set

union (rng b) is set

lim b is epsilon-transitive epsilon-connected ordinal set

s is set

b . s is set

c is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

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

s is epsilon-transitive epsilon-connected ordinal set

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

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

a is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

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

c

exp (a,c

A is epsilon-transitive epsilon-connected ordinal set

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

a is epsilon-transitive epsilon-connected ordinal set

c

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

last s is epsilon-transitive epsilon-connected ordinal set

dom s is epsilon-transitive epsilon-connected ordinal set

union (dom s) is epsilon-transitive epsilon-connected ordinal set

s . (union (dom s)) is epsilon-transitive epsilon-connected ordinal set

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

b is epsilon-transitive epsilon-connected ordinal set

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

last c is epsilon-transitive epsilon-connected ordinal set

dom c is epsilon-transitive epsilon-connected ordinal set

union (dom c) is epsilon-transitive epsilon-connected ordinal set

c . (union (dom c)) is epsilon-transitive epsilon-connected ordinal set

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

A is epsilon-transitive epsilon-connected ordinal set

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

last B is epsilon-transitive epsilon-connected ordinal set

dom B is epsilon-transitive epsilon-connected ordinal set

union (dom B) is epsilon-transitive epsilon-connected ordinal set

B . (union (dom 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,0) is epsilon-transitive epsilon-connected ordinal set

c

A is epsilon-transitive epsilon-connected ordinal set

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

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

s is epsilon-transitive epsilon-connected ordinal set

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

last c is epsilon-transitive epsilon-connected ordinal set

dom c is epsilon-transitive epsilon-connected ordinal set

union (dom c) is epsilon-transitive epsilon-connected ordinal set

c . (union (dom c)) 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

c . {} 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 is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

b is epsilon-transitive epsilon-connected ordinal set

c

(a,c

succ c

c is epsilon-transitive epsilon-connected ordinal set

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

last A is epsilon-transitive epsilon-connected ordinal set

dom A is epsilon-transitive epsilon-connected ordinal set

union (dom A) is epsilon-transitive epsilon-connected ordinal set

A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

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

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

(a,s) 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

c

dom c

lim c

s 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

A is epsilon-transitive epsilon-connected ordinal set

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

last B is epsilon-transitive epsilon-connected ordinal set

dom B is epsilon-transitive epsilon-connected ordinal set

union (dom B) is epsilon-transitive epsilon-connected ordinal set

B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

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

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

(A,c) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

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

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

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

a is epsilon-transitive epsilon-connected ordinal set

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

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

A is epsilon-transitive epsilon-connected ordinal set

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

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

(1,(succ A)) is epsilon-transitive epsilon-connected ordinal set

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

A is epsilon-transitive epsilon-connected ordinal set

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

c

dom c

lim c

rng c

{1} is non empty V12() finite finite-membered V35(1) set

b is set

s is set

c

c is epsilon-transitive epsilon-connected ordinal set

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

b is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

the epsilon-transitive epsilon-connected ordinal Element of A is epsilon-transitive epsilon-connected ordinal Element of A

A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

c

c

a is epsilon-transitive epsilon-connected ordinal set

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

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

succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

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

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

a is epsilon-transitive epsilon-connected ordinal set

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

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

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

succ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

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

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

2 * 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding increasing V53() () () () Element of NAT

(0,(2 * 0)) is epsilon-transitive epsilon-connected ordinal set

(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

(0,((2 * 0) + 1)) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

2 * a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

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

(2 * a) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

(0,((2 * a) + 1)) is epsilon-transitive epsilon-connected ordinal set

a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

2 * (a + 1) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

(0,(2 * (a + 1))) is epsilon-transitive epsilon-connected ordinal set

(2 * (a + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

(0,((2 * (a + 1)) + 1)) is epsilon-transitive epsilon-connected ordinal set

((2 * a) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

(0,(((2 * a) + 1) + 1)) is epsilon-transitive epsilon-connected ordinal set

succ ((2 * a) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

(0,(succ ((2 * a) + 1))) is epsilon-transitive epsilon-connected ordinal set

exp (0,0) is epsilon-transitive epsilon-connected ordinal set

succ (2 * (a + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

(0,(succ (2 * (a + 1)))) is epsilon-transitive epsilon-connected ordinal set

exp (0,1) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

c

(c

(c

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

b is epsilon-transitive epsilon-connected ordinal set

(c

s is epsilon-transitive epsilon-connected ordinal set

(c

b is epsilon-transitive epsilon-connected ordinal set

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

(c

(c

exp (c

s is epsilon-transitive epsilon-connected ordinal set

(c

c is epsilon-transitive epsilon-connected ordinal set

(c

b is epsilon-transitive epsilon-connected ordinal set

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

dom s is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

s . c is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

s . A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

c

(c

(c

(c

(c

Union s is epsilon-transitive epsilon-connected ordinal set

rng s is set

union (rng s) is set

(c

lim s is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

(c

A is epsilon-transitive epsilon-connected ordinal set

(c

s . c is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

dom A is epsilon-transitive epsilon-connected ordinal set

c

A . c

b is epsilon-transitive epsilon-connected ordinal set

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

(a,c

(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

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

c

(a,c

succ c

(a,(succ c

exp (a,(a,c

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

c

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

dom b is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

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

c is epsilon-transitive epsilon-connected ordinal set

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

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

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

Union b is epsilon-transitive epsilon-connected ordinal set

rng b is set

union (rng b) is set

lim b is epsilon-transitive epsilon-connected ordinal set

(a,c

b . 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 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

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

c

(a,c

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

(A + 1) + b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

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

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

succ s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

succ (s + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

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

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

(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

(A + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

(A + 1) + s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

((A + 1) + s) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

(A + 1) + (s + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

a is epsilon-transitive epsilon-connected ordinal set

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

dom A is epsilon-transitive epsilon-connected ordinal set

c

A . c

b is epsilon-transitive epsilon-connected ordinal set

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

s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

A . s is epsilon-transitive epsilon-connected ordinal set

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

c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

A . c is epsilon-transitive epsilon-connected ordinal set

(a,c) 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

succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

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

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

a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

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

a |^ 0 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

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

a |^ A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

succ A is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

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

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

c

b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

c

a |^ (A + 1) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

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

a |^ A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

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

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

c

(a,c

c

succ c

(a,(c

b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

exp (a,b) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

(a,A) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

(a,0) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

c

(a,c

succ c

c

(a,(c

exp (a,(a,c

a |^ (a,c

a |^ c

a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

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

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

dom A is epsilon-transitive epsilon-connected ordinal set

rng A is set

c

b is set

A . b is set

s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

(a,s) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

lim A is epsilon-transitive epsilon-connected ordinal set

c

b is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

(a,s) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

(a,B) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

A . B 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,NAT) is epsilon-transitive epsilon-connected ordinal set

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

dom A is epsilon-transitive epsilon-connected ordinal set

c

A . c

b is epsilon-transitive epsilon-connected ordinal set

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

c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

A . s is epsilon-transitive epsilon-connected ordinal set

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

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

lim 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

a is epsilon-transitive epsilon-connected ordinal set

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

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

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

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

dom A is epsilon-transitive epsilon-connected ordinal set

c

dom c

lim c

Union c

rng c

union (rng c

lim A is epsilon-transitive epsilon-connected ordinal set

Union A is epsilon-transitive epsilon-connected ordinal set

rng A is set

union (rng A) is set

b is set

s is set

c

c is set

A . c is set

A is epsilon-transitive epsilon-connected ordinal set

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

B is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

A . B is epsilon-transitive epsilon-connected ordinal set

exp (a,(A . B)) is epsilon-transitive epsilon-connected ordinal set

succ B is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

c

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

A . (succ B) is epsilon-transitive epsilon-connected ordinal set

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

a is epsilon-transitive epsilon-connected ordinal set

(a,NAT) 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 -^ NAT is epsilon-transitive epsilon-connected ordinal set

NAT +^ (A -^ NAT) is epsilon-transitive epsilon-connected ordinal set

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

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

c

NAT +^ c

(a,(NAT +^ c

succ c

NAT +^ (succ c

(a,(NAT +^ (succ c

exp (a,(a,(NAT +^ c

succ (NAT +^ c

(a,(succ (NAT +^ c

c

NAT +^ c

(a,(NAT +^ c

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

dom b is epsilon-transitive epsilon-connected ordinal set

lim b is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

A is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V33() V34() set

B is epsilon-transitive epsilon-connected ordinal set

B -^ A is epsilon-transitive epsilon-connected ordinal set

(NAT +^ c

NAT +^ (B -^ A) is epsilon-transitive epsilon-connected ordinal set

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

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

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

F

dom F

F

F

Union F

rng F

union (rng F

F

A is epsilon-transitive epsilon-connected ordinal set

F

F

F

A is set

F

b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

F

succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

F

b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

F

c

F

{F

A is set

c

F

A is epsilon-transitive epsilon-connected ordinal set

F

A is epsilon-transitive epsilon-connected ordinal set

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

F

F

F

A is epsilon-transitive epsilon-connected ordinal set

F

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

F

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

F

b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

F

succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

F

b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

succ (b + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

F

F

F

F

F

c

F

succ c

F

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

dom A is epsilon-transitive epsilon-connected ordinal set

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

F

c

b is set

F

succ c

s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

F

succ s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

F

c

A . c

b is epsilon-transitive epsilon-connected ordinal set

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

F

F

sup A is epsilon-transitive epsilon-connected ordinal set

rng A is set

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

lim A is epsilon-transitive epsilon-connected ordinal set

c

b is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

c is set

A . c is set

A is epsilon-transitive epsilon-connected ordinal set

B is set

F

c

F

succ c

F

F

F

c

F

b is set

s is set

F

A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

F

F

succ A is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

F

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

F

c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

F

union c

F

succ F

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

dom a is epsilon-transitive epsilon-connected ordinal set

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

A is epsilon-transitive epsilon-connected ordinal set

F

F

A is epsilon-transitive epsilon-connected ordinal set

F

A is epsilon-transitive epsilon-connected ordinal set

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

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

b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

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

b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

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

F

c

a . c

A is epsilon-transitive epsilon-connected ordinal set

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

c

a . c

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

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

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

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

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

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

s is epsilon-transitive epsilon-connected ordinal set

F

b is epsilon-transitive epsilon-connected ordinal set

A +^ b 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 +^ b 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

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

dom A is epsilon-transitive epsilon-connected ordinal set

F

c

A . c

b is epsilon-transitive epsilon-connected ordinal set

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

F

F

sup A is epsilon-transitive epsilon-connected ordinal set

rng A is set

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

lim A is epsilon-transitive epsilon-connected ordinal set

c

b is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal set

c is set

A . c is set

A is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

c

a . c

c is epsilon-transitive epsilon-connected ordinal set

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

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

F

F

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

a is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

c

exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,c

A is epsilon-transitive epsilon-connected ordinal set

c

dom c

b is epsilon-transitive epsilon-connected ordinal set

c

s is epsilon-transitive epsilon-connected ordinal set

c

exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,s) is epsilon-transitive epsilon-connected ordinal set

Union c

rng c

union (rng c

exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set

lim c

A is epsilon-transitive epsilon-connected ordinal set

exp (NAT,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

c

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

A is epsilon-transitive epsilon-connected ordinal () set

c

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

A is epsilon-transitive epsilon-connected ordinal set

(A) is epsilon-transitive epsilon-connected ordinal () set

c

(0) is epsilon-transitive epsilon-connected ordinal () set

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

a is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

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

exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

dom A is epsilon-transitive epsilon-connected ordinal set

c

A . c

b is epsilon-transitive epsilon-connected ordinal set

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

exp (NAT,c

exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set

Union A is epsilon-transitive epsilon-connected ordinal set

rng A is set

union (rng A) is set

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

lim A is epsilon-transitive epsilon-connected ordinal set

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

dom a is epsilon-transitive epsilon-connected ordinal set

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

a . 0 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 . (succ A) is epsilon-transitive epsilon-connected ordinal set

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

exp (NAT,(a . A)) is epsilon-transitive epsilon-connected ordinal set

Union a is epsilon-transitive epsilon-connected ordinal set

rng a is set

union (rng a) is set

exp (NAT,(Union a)) is epsilon-transitive epsilon-connected ordinal set

(NAT,0) is epsilon-transitive epsilon-connected ordinal set

c

a . c

(NAT,c

c

a . (c

(NAT,(c

succ c

exp (NAT,(a . c

c

a . c

(NAT,c

lim a is epsilon-transitive epsilon-connected ordinal set

c

a . c

b is epsilon-transitive epsilon-connected ordinal set

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

(NAT,c

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

s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

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

c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

(NAT,c) is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal () set

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

c

exp (NAT,c

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

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

exp (NAT,0) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,1) is epsilon-transitive epsilon-connected ordinal set

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

a is epsilon-transitive epsilon-connected ordinal set

exp (NAT,0) is epsilon-transitive epsilon-connected ordinal set

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

a is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set

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

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

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

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

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

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

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

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

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

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

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

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

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

a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

A is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set

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

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

exp (NAT,(A,(a + 1))) is epsilon-transitive epsilon-connected ordinal set

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

(a + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

succ (a + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

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

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

exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set

exp ((exp (NAT,A)),(A,(a + 1))) is epsilon-transitive epsilon-connected ordinal set

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

exp (NAT,((A,(a + 1)) *^ A)) is epsilon-transitive epsilon-connected ordinal set

succ a is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

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

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

exp (NAT,((A,(succ a)) *^ A)) is epsilon-transitive epsilon-connected ordinal set

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

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

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

exp (A,1) is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

exp (NAT,(exp (A,(1 +^ (A,a))))) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,(exp (A,(A,a)))) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,(A,(succ a))) is epsilon-transitive epsilon-connected ordinal set

a is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set

(a) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set

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

A is epsilon-transitive epsilon-connected ordinal set

c

exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,c

A is epsilon-transitive epsilon-connected ordinal set

c

dom c

b is epsilon-transitive epsilon-connected ordinal set

c

s is epsilon-transitive epsilon-connected ordinal set

c

exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,s) is epsilon-transitive epsilon-connected ordinal set

Union c

rng c

union (rng c

exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set

lim c

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

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

dom A is epsilon-transitive epsilon-connected ordinal set

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

A . 0 is epsilon-transitive epsilon-connected ordinal set

c

succ c

A . (succ c

A . c

exp (NAT,(A . c

Union A is epsilon-transitive epsilon-connected ordinal set

rng A is set

union (rng A) is set

exp (NAT,(Union A)) is epsilon-transitive epsilon-connected ordinal set

c

b is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set

exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

succ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

A . 1 is epsilon-transitive epsilon-connected ordinal set

exp (NAT,(succ a)) is epsilon-transitive epsilon-connected ordinal set

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

NAT *^ H

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

A . 2 is epsilon-transitive epsilon-connected ordinal set

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

exp (H

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

A . 3 is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

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

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

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

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

A . (0 + 1) is epsilon-transitive epsilon-connected ordinal set

0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

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

b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

A . (b + 1) is epsilon-transitive epsilon-connected ordinal set

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

b + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

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

(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

A . ((b + 1) + 1) is epsilon-transitive epsilon-connected ordinal set

(b + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

succ (b + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set

exp (NAT,(A . b)) is epsilon-transitive epsilon-connected ordinal set

A . ((b + 1) + 1) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,(A . (b + 1))) is epsilon-transitive epsilon-connected ordinal set

s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

2 + s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

s + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

exp (NAT,(a,(s + 2))) is epsilon-transitive epsilon-connected ordinal set

(s + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

exp (NAT,(a,(b + 2))) is epsilon-transitive epsilon-connected ordinal set

(b + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

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

dom b is epsilon-transitive epsilon-connected ordinal set

lim b is epsilon-transitive epsilon-connected ordinal set

Union b is epsilon-transitive epsilon-connected ordinal set

rng b is set

union (rng b) is set

s is set

c is set

A . c is set

A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

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

A + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

b . (A + 2) is epsilon-transitive epsilon-connected ordinal set

s is set

c is set

b . c is set

A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

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

A . (A + 1) is epsilon-transitive epsilon-connected ordinal set

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 epsilon-transitive epsilon-connected ordinal set

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

last b is epsilon-transitive epsilon-connected ordinal set

dom b is epsilon-transitive epsilon-connected ordinal set

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

b . (union (dom b)) is epsilon-transitive epsilon-connected ordinal set

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

c

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

last s is epsilon-transitive epsilon-connected ordinal set

dom s is epsilon-transitive epsilon-connected ordinal set

union (dom s) is epsilon-transitive epsilon-connected ordinal set

s . (union (dom s)) is epsilon-transitive epsilon-connected ordinal set

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

c is epsilon-transitive epsilon-connected ordinal set

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

last A is epsilon-transitive epsilon-connected ordinal set

dom A is epsilon-transitive epsilon-connected ordinal set

union (dom A) is epsilon-transitive epsilon-connected ordinal set

A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set

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

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

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

b is epsilon-transitive epsilon-connected ordinal set

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

last s is epsilon-transitive epsilon-connected ordinal set

dom s is epsilon-transitive epsilon-connected ordinal set

union (dom s) is epsilon-transitive epsilon-connected ordinal set

s . (union (dom s)) is epsilon-transitive epsilon-connected ordinal set

c

succ c

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

(c

a is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

c

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

s is epsilon-transitive epsilon-connected <