:: ORDINAL2 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 Function-like functional set

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

meet {} is set

union {} is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

union (succ n) is epsilon-transitive epsilon-connected ordinal set

n is set

a is set

b is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

bool n is non empty Element of bool (bool n)

bool n is non empty set

bool (bool n) is non empty set

n is set

a is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

union n is epsilon-transitive epsilon-connected ordinal set

n is set

a is set

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

dom n is epsilon-transitive epsilon-connected ordinal set

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

n . (union (dom n)) is set

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

dom n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

(n) is set

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

n . (union (dom n)) is set

n . n is set

n is set

On n is set

n is set

n is epsilon-transitive epsilon-connected ordinal set

On n is set

n is set

a is set

n is set

On n is set

n is set

On n is set

a is set

n is set

Lim n is set

n is set

n is set

Lim n is set

n is set

Lim n is set

a is set

b is epsilon-transitive epsilon-connected ordinal set

n is set

Lim n is set

On n is set

n is set

a is epsilon-transitive epsilon-connected ordinal set

n is set

meet n is set

the Element of n is Element of n

a is epsilon-transitive epsilon-connected ordinal set

b is set

xi is set

B is epsilon-transitive epsilon-connected ordinal set

n is set

On n is set

meet (On n) is set

n is set

n is set

union (On n) is set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

a is set

b is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

n is set

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

On n is set

meet (On n) is set

n is epsilon-transitive epsilon-connected ordinal set

n is set

On n is set

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

meet (On n) is set

a is set

b is set

xi is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

n is set

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

On n is set

meet (On n) is set

a is set

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

On a is set

meet (On a) is set

n is epsilon-transitive epsilon-connected ordinal set

n is set

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

On n is set

meet (On n) is set

a is epsilon-transitive epsilon-connected ordinal set

b is set

xi is set

B is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

On n is set

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

n is set

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

On n is set

n is epsilon-transitive epsilon-connected ordinal set

n is set

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

On n is set

a is set

b is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

n is set

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

a is epsilon-transitive epsilon-connected ordinal set

n is set

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

n is set

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

On n is set

On n is set

n is epsilon-transitive epsilon-connected ordinal set

{n} is non empty set

({n}) is epsilon-transitive epsilon-connected ordinal set

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

n \/ {n} is non empty set

On {n} is set

n is set

n is epsilon-transitive epsilon-connected ordinal set

n is set

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

On n is set

meet (On n) is set

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

n is set

the Element of On n is Element of On n

b is epsilon-transitive epsilon-connected ordinal set

F

n is Relation-like Function-like set

dom n is set

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

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

dom a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a . b is set

F

{b} is non empty set

union {b} is set

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

F

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

F

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

the T-Sequence-like Relation-like the epsilon-transitive epsilon-connected ordinal set -valued Function-like set is T-Sequence-like Relation-like the epsilon-transitive epsilon-connected ordinal set -valued Function-like set

rng the T-Sequence-like Relation-like the epsilon-transitive epsilon-connected ordinal set -valued Function-like set is set

n is epsilon-transitive epsilon-connected ordinal set

n is T-Sequence-like Relation-like n -valued Function-like set

rng n is set

n is T-Sequence-like Relation-like Function-like () set

n is epsilon-transitive epsilon-connected ordinal set

n | n is T-Sequence-like Relation-like rng n -valued Function-like set

rng n is set

a is epsilon-transitive epsilon-connected ordinal set

rng (n | n) is set

n is epsilon-transitive epsilon-connected ordinal set

n is T-Sequence-like Relation-like Function-like () set

dom n is epsilon-transitive epsilon-connected ordinal set

n . n is set

rng n is set

a is epsilon-transitive epsilon-connected ordinal set

n is T-Sequence-like Relation-like Function-like () set

n is epsilon-transitive epsilon-connected ordinal set

n . n is set

dom n is epsilon-transitive epsilon-connected ordinal set

F

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

dom n is epsilon-transitive epsilon-connected ordinal set

rng n is set

((rng n)) is epsilon-transitive epsilon-connected ordinal set

n is set

a is set

n . a is set

b is epsilon-transitive epsilon-connected ordinal set

n . b is set

F

On (rng n) is set

n is T-Sequence-like Relation-like Function-like () set

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

dom 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

F

F

dom F

F

F

F

F

dom F

F

n is set

n is set

n is set

F

F

n is epsilon-transitive epsilon-connected ordinal set

F

rng F

dom (F

F

rng F

dom (F

a is epsilon-transitive epsilon-connected ordinal set

F

F

a is set

(F

F

(F

F

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

F

(F

F

(F

F

F

F

F

F

F

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

F

F

n is epsilon-transitive epsilon-connected ordinal set

n is set

a is set

b is set

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

dom B is epsilon-transitive epsilon-connected ordinal set

xi is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

B . C is set

B | C is T-Sequence-like Relation-like rng B -valued Function-like set

rng B is set

F

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

B . (succ C) is set

B . C is set

F

B . {} is set

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

C . {} is set

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

C . (succ D) is set

C . D is set

F

D is epsilon-transitive epsilon-connected ordinal set

C . D is set

C | D is T-Sequence-like Relation-like rng C -valued Function-like set

rng C is set

F

dom C is epsilon-transitive epsilon-connected ordinal set

n is Relation-like Function-like set

dom n is set

a is set

b is set

[a,b] is set

{a,b} is non empty set

{a} is non empty set

{{a,b},{a}} is non empty set

a is set

b is epsilon-transitive epsilon-connected ordinal set

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

dom xi is epsilon-transitive epsilon-connected ordinal set

xi . {} is set

B is epsilon-transitive epsilon-connected ordinal set

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

dom C is epsilon-transitive epsilon-connected ordinal set

C . {} is set

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

C . (succ D) is set

C . D is set

F

E is epsilon-transitive epsilon-connected ordinal set

C . E is set

C | E is T-Sequence-like Relation-like rng C -valued Function-like set

rng C is set

F

[b,xi] is set

{b,xi} is non empty set

{b} is non empty set

{{b,xi},{b}} is non empty set

a is set

n . a is set

xi is set

[a,xi] is set

{a,xi} is non empty set

{a} is non empty set

{{a,xi},{a}} is non empty set

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

{C} is non empty set

C \/ {C} is non empty set

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

B . C is set

F

F

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

F

C is epsilon-transitive epsilon-connected ordinal set

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

E is epsilon-transitive epsilon-connected ordinal set

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

{E} is non empty set

E \/ {E} is non empty set

D . E is set

F

F

D is epsilon-transitive epsilon-connected ordinal set

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

L2 is set

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

C . C is set

F

F

c

succ c

{c

c

c

c

c

succ c

{c

c

c

F

F

a is set

n . a is set

b is set

xi is set

B is epsilon-transitive epsilon-connected ordinal set

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

F

D is epsilon-transitive epsilon-connected ordinal set

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

F

L2 is epsilon-transitive epsilon-connected ordinal set

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

{L2} is non empty set

L2 \/ {L2} is non empty set

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

C . D is set

F

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

C . D is set

F

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

E . C is set

F

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

E . C is set

F

L2 is epsilon-transitive epsilon-connected ordinal set

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

{L2} is non empty set

L2 \/ {L2} is non empty set

C . L2 is set

F

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

E . D is set

F

a is Relation-like Function-like set

dom a is set

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

dom b is epsilon-transitive epsilon-connected ordinal set

b . {} is set

n . {} is set

a . {} is set

xi is epsilon-transitive epsilon-connected ordinal set

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

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

B . C is set

F

F

xi is epsilon-transitive epsilon-connected ordinal set

n . xi is set

b | xi is T-Sequence-like Relation-like rng b -valued Function-like set

rng b is set

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

[xi,B] is set

{xi,B} is non empty set

{xi} is non empty set

{{xi,B},{xi}} is non empty set

dom B is epsilon-transitive epsilon-connected ordinal set

B . {} is set

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

B . (succ C) is set

B . C is set

F

D is epsilon-transitive epsilon-connected ordinal set

B . D is set

B | D is T-Sequence-like Relation-like rng B -valued Function-like set

rng B is set

F

C is set

D is epsilon-transitive epsilon-connected ordinal set

n . D is set

b . D is set

E is epsilon-transitive epsilon-connected ordinal set

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

F

B | D is T-Sequence-like Relation-like rng B -valued Function-like set

rng B is set

D is epsilon-transitive epsilon-connected ordinal set

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

dom C is epsilon-transitive epsilon-connected ordinal set

C . {} is set

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

C . (succ C) is set

C . C is set

F

(B | D) . C is set

B . C is set

(B | D) . (succ C) is set

B . (succ C) is set

C is epsilon-transitive epsilon-connected ordinal set

C . C is set

C | C is T-Sequence-like Relation-like rng C -valued Function-like set

rng C is set

F

B | C is T-Sequence-like Relation-like rng B -valued Function-like set

B . C is set

[D,(B | D)] is set

{D,(B | D)} is non empty set

{D} is non empty set

{{D,(B | D)},{D}} is non empty set

(b | xi) . C is set

b . C is set

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

B . C is set

B . D is set

F

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

L2 . C is set

F

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

L2 . C is set

F

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

L2 . D is set

F

dom (b | xi) is epsilon-transitive epsilon-connected ordinal set

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

b . (succ xi) is set

b . xi is set

F

n . (succ xi) is set

a . (succ xi) is set

B is epsilon-transitive epsilon-connected ordinal set

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

F

b | (succ xi) is T-Sequence-like Relation-like rng b -valued Function-like set

rng b is set

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

C . D is set

F

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

C . D is set

F

xi is epsilon-transitive epsilon-connected ordinal set

b . xi is set

b | xi is T-Sequence-like Relation-like rng b -valued Function-like set

rng b is set

F

n . xi is set

a . xi is set

B is epsilon-transitive epsilon-connected ordinal set

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

D is epsilon-transitive epsilon-connected ordinal set

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

{D} is non empty set

D \/ {D} is non empty set

C . D is set

F

F

F

F

dom F

F

F

n is epsilon-transitive epsilon-connected ordinal set

F

F

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

{n} is non empty set

n \/ {n} is non empty set

F

rng F

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

(F

(F

F

F

F

a is epsilon-transitive epsilon-connected ordinal set

(F

(F

rng (F

F

F

F

(F

dom (F

((F

union (dom (F

(F

(F

F

succ F

{F

F

F

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

dom n is epsilon-transitive epsilon-connected ordinal set

n . {} is set

(n) is set

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

n . (union (dom n)) is set

n 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

n . (succ a) is set

n . a is set

F

b is epsilon-transitive epsilon-connected ordinal set

n . b is set

n | b is T-Sequence-like Relation-like rng n -valued Function-like set

rng n is set

F

n is set

a is set

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

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

b . {} is set

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

(xi) is set

dom xi is epsilon-transitive epsilon-connected ordinal set

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

xi . (union (dom xi)) is set

xi . {} is set

F

F

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

{{}} is non empty set

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

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

dom n is epsilon-transitive epsilon-connected ordinal set

n . {} is set

(n) is set

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

n . (union (dom n)) is set

F

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

F

F

F

succ (succ n) is non empty epsilon-transitive epsilon-connected ordinal set

{(succ n)} is non empty set

(succ n) \/ {(succ n)} is non empty set

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

dom n is epsilon-transitive epsilon-connected ordinal set

n . {} is set

b is set

a is epsilon-transitive epsilon-connected ordinal set

F

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

{a} is non empty set

a \/ {a} is non empty set

B is set

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

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

C . {} is set

F

n . (succ n) is set

n . n is set

F

F

F

dom F

F

F

succ F

{F

F

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

dom n is epsilon-transitive epsilon-connected ordinal set

n . {} is set

n | F

rng n is set

b is set

a is epsilon-transitive epsilon-connected ordinal set

F

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

{a} is non empty set

a \/ {a} is non empty set

B is set

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

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

C . {} is set

F

a is set

(n | F

b is epsilon-transitive epsilon-connected ordinal set

n . b is set

F

F

dom (n | F

n . F

F

F

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

dom n is epsilon-transitive epsilon-connected ordinal set

n . {} is set

rng n is set

((rng n)) is epsilon-transitive epsilon-connected ordinal set

n is set

a is set

n . a is set

b is epsilon-transitive epsilon-connected ordinal set

n . b is set

n | b is T-Sequence-like Relation-like rng n -valued Function-like set

F

On (rng n) is set

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

n . xi is set

{(n . xi)} is non empty set

union {(n . xi)} is set

((union {(n . xi)})) is epsilon-transitive epsilon-connected ordinal set

F

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

n is T-Sequence-like Relation-like Function-like () set

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

dom a is epsilon-transitive epsilon-connected ordinal set

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

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

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

F

xi is epsilon-transitive epsilon-connected ordinal set

{xi} is non empty set

union {xi} is set

((union {xi})) is epsilon-transitive epsilon-connected ordinal set

(xi) 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 is T-Sequence-like Relation-like rng a -valued Function-like () set

rng a is set

F

F

F

dom F

F

F

n is epsilon-transitive epsilon-connected ordinal set

F

F

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

{n} is non empty set

n \/ {n} is non empty set

F

rng F

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

(F

(F

F

F

F

a is epsilon-transitive epsilon-connected ordinal set

(F

(F

rng (F

F

F

F

(F

dom (F

((F

union (dom (F

(F

(F

F

succ F

{F

F

F

n is T-Sequence-like Relation-like Function-like () set

dom n is epsilon-transitive epsilon-connected ordinal set

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

(n) is set

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

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

n 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

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

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

F

b is epsilon-transitive epsilon-connected ordinal set

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

n | b is T-Sequence-like Relation-like rng n -valued Function-like () set

rng n is set

F

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

xi is T-Sequence-like Relation-like Function-like () set

(xi) is set

dom xi is epsilon-transitive epsilon-connected ordinal set

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

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

xi . {} 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

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

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

{(xi . B)} is non empty set

union {(xi . B)} is set

((union {(xi . B)})) is epsilon-transitive epsilon-connected ordinal set

F

C is epsilon-transitive epsilon-connected ordinal set

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

B is T-Sequence-like Relation-like Function-like () set

(B) is 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 is epsilon-transitive epsilon-connected ordinal set

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

B | C is T-Sequence-like Relation-like rng B -valued Function-like () set

rng B is set

F

C is epsilon-transitive epsilon-connected ordinal set

xi . C is epsilon-transitive epsilon-connected ordinal set

xi | C is T-Sequence-like Relation-like rng xi -valued Function-like () set

rng xi is set

F

C is epsilon-transitive epsilon-connected ordinal set

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

{C} is non empty set

C \/ {C} is non empty set

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

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

{(B . C)} is non empty set

union {(B . C)} is set

((union {(B . C)})) is epsilon-transitive epsilon-connected ordinal set

F

D is epsilon-transitive epsilon-connected ordinal set

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

F

F

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

{{}} is non empty set

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

n is T-Sequence-like Relation-like Function-like () set

dom n is epsilon-transitive epsilon-connected ordinal set

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

(n) is set

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

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

F

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

F

F

F

succ (succ n) is non empty epsilon-transitive epsilon-connected ordinal set

{(succ n)} is non empty set

(succ n) \/ {(succ n)} is non empty set

n is T-Sequence-like Relation-like Function-like () set

dom n is epsilon-transitive epsilon-connected ordinal set

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

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

F

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

C is T-Sequence-like Relation-like Function-like () set

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

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

F

n . (succ n) is epsilon-transitive epsilon-connected ordinal set

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

F

F

F

dom F

F

F

succ F

{F

F

n is T-Sequence-like Relation-like Function-like () set

dom n is epsilon-transitive epsilon-connected ordinal set

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

n | F

rng n is set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

F

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

C is T-Sequence-like Relation-like Function-like () set

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

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

F

a is set

(n | F

b is epsilon-transitive epsilon-connected ordinal set

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

F

F

dom (n | F

n . F

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

rng n is set

((rng n)) is epsilon-transitive epsilon-connected ordinal set

((rng n)) is epsilon-transitive epsilon-connected ordinal set

On (rng n) is set

meet (On (rng n)) is set

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

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

rng n is set

((rng n)) is epsilon-transitive epsilon-connected ordinal set

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

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

rng n is set

((rng n)) is epsilon-transitive epsilon-connected ordinal set

On (rng n) is set

meet (On (rng n)) is set

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

dom n is epsilon-transitive epsilon-connected ordinal set

n is T-Sequence-like Relation-like Function-like () set

dom n is epsilon-transitive epsilon-connected ordinal set

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

rng n is set

((rng n)) is epsilon-transitive epsilon-connected ordinal set

On (rng n) is set

meet (On (rng n)) is set

a is epsilon-transitive epsilon-connected ordinal set

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

(dom n) \ a is Element of bool (dom n)

bool (dom n) is non empty set

n | ((dom n) \ a) is Relation-like Function-like set

rng (n | ((dom n) \ a)) is set

((rng (n | ((dom n) \ a)))) is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like () set

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

rng b is set

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

On (rng b) is set

meet (On (rng b)) is set

dom b is epsilon-transitive epsilon-connected ordinal set

xi is T-Sequence-like Relation-like Function-like () set

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

rng xi is set

((rng xi)) is epsilon-transitive epsilon-connected ordinal set

On (rng xi) is set

meet (On (rng xi)) is set

dom xi is epsilon-transitive epsilon-connected ordinal set

B is set

C is epsilon-transitive epsilon-connected ordinal set

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

(dom n) \ C is Element of bool (dom n)

bool (dom n) is non empty set

n | ((dom n) \ C) is Relation-like Function-like set

rng (n | ((dom n) \ C)) is set

((rng (n | ((dom n) \ C)))) is epsilon-transitive epsilon-connected ordinal set

b . B is set

xi . B is set

n is T-Sequence-like Relation-like Function-like () set

dom n is epsilon-transitive epsilon-connected ordinal set

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

rng n is set

((rng n)) is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

(dom n) \ a is Element of bool (dom n)

bool (dom n) is non empty set

n | ((dom n) \ a) is Relation-like Function-like set

rng (n | ((dom n) \ a)) is set

((rng (n | ((dom n) \ a)))) is epsilon-transitive epsilon-connected ordinal set

On (rng (n | ((dom n) \ a))) is set

meet (On (rng (n | ((dom n) \ a)))) is set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is T-Sequence-like Relation-like Function-like () set

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

rng b is set

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

dom b is epsilon-transitive epsilon-connected ordinal set

xi is T-Sequence-like Relation-like Function-like () set

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

rng xi is set

((rng xi)) is epsilon-transitive epsilon-connected ordinal set

dom xi is epsilon-transitive epsilon-connected ordinal set

B is set

C is epsilon-transitive epsilon-connected ordinal set

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

(dom n) \ C is Element of bool (dom n)

bool (dom n) is non empty set

n | ((dom n) \ C) is Relation-like Function-like set

rng (n | ((dom n) \ C)) is set

((rng (n | ((dom n) \ C)))) is epsilon-transitive epsilon-connected ordinal set

On (rng (n | ((dom n) \ C))) is set

meet (On (rng (n | ((dom n) \ C)))) is set

b . B is set

xi . B is set

n is T-Sequence-like Relation-like Function-like () set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

dom n 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

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

{b} is non empty set

b \/ {b} is non empty set

C is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

E is epsilon-transitive epsilon-connected ordinal set

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

B 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

D is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

E is epsilon-transitive epsilon-connected ordinal set

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

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

C is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

E is epsilon-transitive epsilon-connected ordinal set

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

B is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

E is epsilon-transitive epsilon-connected ordinal set

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

n is T-Sequence-like Relation-like Function-like () set

n is epsilon-transitive epsilon-connected ordinal set

n | n is T-Sequence-like Relation-like rng n -valued Function-like () set

rng n is set

((n | n)) is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

xi is T-Sequence-like Relation-like Function-like () set

(xi) is set

dom xi is epsilon-transitive epsilon-connected ordinal set

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

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

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

b is epsilon-transitive epsilon-connected ordinal set

B is T-Sequence-like Relation-like Function-like () set

(B) is 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 is epsilon-transitive epsilon-connected ordinal set

D is T-Sequence-like Relation-like Function-like () set

(D) is set

dom D is epsilon-transitive epsilon-connected ordinal set

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

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

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

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

xi is T-Sequence-like Relation-like Function-like () set

(xi) is set

dom xi is epsilon-transitive epsilon-connected ordinal set

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

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

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

b is epsilon-transitive epsilon-connected ordinal set

B is T-Sequence-like Relation-like Function-like () set

(B) is 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 is epsilon-transitive epsilon-connected ordinal set

D is T-Sequence-like Relation-like Function-like () set

(D) is set

dom D is epsilon-transitive epsilon-connected ordinal set

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

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

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

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal Element of n

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

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

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

xi is T-Sequence-like Relation-like Function-like () set

(xi) is set

dom xi is epsilon-transitive epsilon-connected ordinal set

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

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

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

b is epsilon-transitive epsilon-connected ordinal set

B is T-Sequence-like Relation-like Function-like () set

(B) is 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 is epsilon-transitive epsilon-connected ordinal set

D is T-Sequence-like Relation-like Function-like () set

(D) is set

dom D is epsilon-transitive epsilon-connected ordinal set

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

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

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

n is epsilon-transitive epsilon-connected ordinal set

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

a is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

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

{n} is non empty set

n \/ {n} is non empty set

xi is epsilon-transitive epsilon-connected ordinal set

B is T-Sequence-like Relation-like Function-like () set

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

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

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

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

(n,(succ n)) is epsilon-transitive epsilon-connected ordinal set

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

succ (n,n) is non empty epsilon-transitive epsilon-connected ordinal set

{(n,n)} is non empty set

(n,n) \/ {(n,n)} is non empty set

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(n,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

C is T-Sequence-like Relation-like Function-like () set

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

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

(n,xi) is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

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

dom a is epsilon-transitive epsilon-connected ordinal set

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

rng a is set

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

xi is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(n,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

C is epsilon-transitive epsilon-connected ordinal set

D is T-Sequence-like Relation-like Function-like () set

(D) is set

dom D is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

n is epsilon-transitive epsilon-connected ordinal set

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

n is epsilon-transitive epsilon-connected ordinal set

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

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

{n} is non empty set

n \/ {n} is non empty set

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

n is epsilon-transitive epsilon-connected ordinal set

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

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

dom a is epsilon-transitive epsilon-connected ordinal set

rng a is set

b is set

xi is set

a . xi is set

B is epsilon-transitive epsilon-connected ordinal set

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

b is set

xi is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

({},{}) 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

n is epsilon-transitive epsilon-connected ordinal set

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

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

{n} is non empty set

n \/ {n} is non empty set

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

succ (n,{}) is non empty epsilon-transitive epsilon-connected ordinal set

{(n,{})} is non empty set

(n,{}) \/ {(n,{})} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

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

b is epsilon-transitive epsilon-connected ordinal set

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

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

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

{(a,xi)} is non empty set

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

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

xi is T-Sequence-like Relation-like Function-like () set

dom xi is epsilon-transitive epsilon-connected ordinal set

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

rng xi is set

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

((rng xi)) is epsilon-transitive epsilon-connected ordinal set

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

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

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

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

b is epsilon-transitive epsilon-connected ordinal set

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

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

(n,xi) is epsilon-transitive epsilon-connected ordinal set

succ (n,xi) is non empty epsilon-transitive epsilon-connected ordinal set

{(n,xi)} is non empty set

(n,xi) \/ {(n,xi)} is non empty set

(n,xi) is epsilon-transitive epsilon-connected ordinal set

succ (n,xi) is non empty epsilon-transitive epsilon-connected ordinal set

{(n,xi)} is non empty set

(n,xi) \/ {(n,xi)} is non empty set

xi is T-Sequence-like Relation-like Function-like () set

dom xi is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

rng xi is set

C is set

xi . C is set

D is epsilon-transitive epsilon-connected ordinal set

(n,D) is epsilon-transitive epsilon-connected ordinal set

(n,D) is epsilon-transitive epsilon-connected ordinal set

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

((rng xi)) is epsilon-transitive epsilon-connected ordinal set

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

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

a is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

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

{n} is non empty set

n \/ {n} is non empty set

xi is epsilon-transitive epsilon-connected ordinal set

B is T-Sequence-like Relation-like Function-like () set

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

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,n) is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

((succ n),n) is epsilon-transitive epsilon-connected ordinal set

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

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

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

C is T-Sequence-like Relation-like Function-like () set

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

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

(xi,n) is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

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

dom a is epsilon-transitive epsilon-connected ordinal set

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

rng a is set

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

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

xi is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(b,n) 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

C is epsilon-transitive epsilon-connected ordinal set

D is T-Sequence-like Relation-like Function-like () set

(D) is set

dom D is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

n is epsilon-transitive epsilon-connected ordinal set

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

n is epsilon-transitive epsilon-connected ordinal set

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

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

{n} is non empty set

n \/ {n} is non empty set

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

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

n is epsilon-transitive epsilon-connected ordinal set

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

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

dom a is epsilon-transitive epsilon-connected ordinal set

rng a is set

b is set

xi is set

a . xi is set

B is epsilon-transitive epsilon-connected ordinal set

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

b is set

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

a . b is set

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

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

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

n is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

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

n is epsilon-transitive epsilon-connected ordinal set

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

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

dom a is epsilon-transitive epsilon-connected ordinal set

rng a is set

b is set

xi is epsilon-transitive epsilon-connected ordinal set

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

a . b is set

b is set

xi is set

a . xi is set

B is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

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

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

union n 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,(succ {})) is epsilon-transitive epsilon-connected ordinal set

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

(a,(succ {})) 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

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

{a} is non empty set

a \/ {a} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

a is epsilon-transitive epsilon-connected ordinal set

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

b is epsilon-transitive epsilon-connected ordinal set

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

(xi,n) is epsilon-transitive epsilon-connected ordinal set

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

((xi,n),n) is epsilon-transitive epsilon-connected ordinal set

((succ xi),n) is epsilon-transitive epsilon-connected ordinal set

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

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

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

{n} is non empty set

n \/ {n} is non empty set

((succ n),n) is epsilon-transitive epsilon-connected ordinal set

xi is T-Sequence-like Relation-like Function-like () set

dom xi is epsilon-transitive epsilon-connected ordinal set

xi . (succ n) is epsilon-transitive epsilon-connected ordinal set

rng xi is set

((rng xi)) is epsilon-transitive epsilon-connected ordinal set

union ((rng xi)) is epsilon-transitive epsilon-connected ordinal set

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

union (xi) is epsilon-transitive epsilon-connected ordinal set

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

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

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

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

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

b is epsilon-transitive epsilon-connected ordinal set

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

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

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

(xi,n) is epsilon-transitive epsilon-connected ordinal set

(xi,n) is epsilon-transitive epsilon-connected ordinal set

((xi,n),n) is epsilon-transitive epsilon-connected ordinal set

((xi,n),n) is epsilon-transitive epsilon-connected ordinal set

((xi,n),n) is epsilon-transitive epsilon-connected ordinal set

xi is T-Sequence-like Relation-like Function-like () set

dom xi is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

rng xi is set

C is set

xi . C is set

D is epsilon-transitive epsilon-connected ordinal set

(D,n) is epsilon-transitive epsilon-connected ordinal set

(D,n) is epsilon-transitive epsilon-connected ordinal set

((rng xi)) is epsilon-transitive epsilon-connected ordinal set

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

union (xi) is epsilon-transitive epsilon-connected ordinal set

union ((rng xi)) is epsilon-transitive epsilon-connected ordinal set

xi is epsilon-transitive epsilon-connected ordinal set

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

{xi} is non empty set

xi \/ {xi} is non empty set

n is epsilon-transitive epsilon-connected ordinal set

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

a is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

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

{n} is non empty set

n \/ {n} is non empty set

xi is epsilon-transitive epsilon-connected ordinal set

B is T-Sequence-like Relation-like Function-like () set

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

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

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

n is epsilon-transitive epsilon-connected ordinal set

n is epsilon-transitive epsilon-connected ordinal set

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

{n} is non empty set

n \/ {n} is non empty set

(n,(succ n)) is epsilon-transitive epsilon-connected ordinal set

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

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

b is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

(n,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