omega is non empty epsilon-transitive epsilon-connected ordinal set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set
1 is non empty epsilon-transitive epsilon-connected ordinal natural Element of omega
a is set
succ a is non empty set
{a} is non empty set
a \/ {a} is non empty set
a is set
succ a is non empty set
{a} is non empty set
a \/ {a} is non empty set
b is set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
a is epsilon-transitive epsilon-connected ordinal set
b is set
union b is set
a is set
a is set
On a is set
union (On a) is set
b is set
a is epsilon-transitive epsilon-connected ordinal set
b is set
On b is set
a is set
b is set
a is set
b is set
a is epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
On {a} is set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
a \/ {a} is non empty set
a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
inf a is epsilon-transitive epsilon-connected ordinal set
On a is set
meet (On a) is set
meet a is set
a is epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
inf {a} is epsilon-transitive epsilon-connected ordinal set
On {a} is set
meet (On {a}) is set
meet {a} is set
a is epsilon-transitive epsilon-connected ordinal set
b is set
meet b is set
inf b is epsilon-transitive epsilon-connected ordinal set
On b is set
meet (On b) is set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a \/ b is set
a /\ b is set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a \/ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a /\ b is epsilon-transitive epsilon-connected ordinal set
succ {} is non empty epsilon-transitive epsilon-connected ordinal natural set
{{}} is non empty set
{} \/ {{}} is non empty set
a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a +^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b +^ b is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a +^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b +^ b is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
{} +^ b is epsilon-transitive epsilon-connected ordinal set
a +^ {} is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
a +^ (succ b) is epsilon-transitive epsilon-connected ordinal set
a +^ {} is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
{} +^ a is epsilon-transitive epsilon-connected ordinal set
a +^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
rng b is set
a is epsilon-transitive epsilon-connected ordinal set
x is set
b . x is set
k is epsilon-transitive epsilon-connected ordinal set
b . k is epsilon-transitive epsilon-connected ordinal set
a +^ k is epsilon-transitive epsilon-connected ordinal set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
a +^ a is epsilon-transitive epsilon-connected ordinal set
succ (a +^ a) is non empty epsilon-transitive epsilon-connected ordinal set
{(a +^ a)} is non empty set
(a +^ a) \/ {(a +^ a)} is non empty set
a +^ (succ a) is epsilon-transitive epsilon-connected ordinal set
sup b is epsilon-transitive epsilon-connected ordinal set
a +^ {} is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a +^ a is epsilon-transitive epsilon-connected ordinal set
a +^ {} is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
b is epsilon-transitive epsilon-connected ordinal set
b +^ b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
a . (succ b) is epsilon-transitive epsilon-connected ordinal set
b +^ (succ b) is epsilon-transitive epsilon-connected ordinal set
succ (b +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
{(b +^ b)} is non empty set
(b +^ b) \/ {(b +^ b)} is non empty set
(succ b) +^ {} is epsilon-transitive epsilon-connected ordinal set
b +^ {} is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a +^ b) +^ a is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
a +^ (b +^ a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a +^ b) +^ b is epsilon-transitive epsilon-connected ordinal set
b +^ b is epsilon-transitive epsilon-connected ordinal set
a +^ (b +^ b) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
(a +^ b) +^ (succ b) is epsilon-transitive epsilon-connected ordinal set
b +^ (succ b) is epsilon-transitive epsilon-connected ordinal set
a +^ (b +^ (succ b)) is epsilon-transitive epsilon-connected ordinal set
succ ((a +^ b) +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
{((a +^ b) +^ b)} is non empty set
((a +^ b) +^ b) \/ {((a +^ b) +^ b)} is non empty set
succ (b +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
{(b +^ b)} is non empty set
(b +^ b) \/ {(b +^ b)} is non empty set
a +^ (succ (b +^ b)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a +^ b) +^ b is epsilon-transitive epsilon-connected ordinal set
b +^ b is epsilon-transitive epsilon-connected ordinal set
a +^ (b +^ b) is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
rng b is set
rng a is set
x is set
k is set
b . k is set
m is epsilon-transitive epsilon-connected ordinal set
b +^ m is epsilon-transitive epsilon-connected ordinal set
b . m is epsilon-transitive epsilon-connected ordinal set
(a +^ b) +^ m is epsilon-transitive epsilon-connected ordinal set
a +^ (b +^ m) is epsilon-transitive epsilon-connected ordinal set
a . (b +^ m) is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
sup b is epsilon-transitive epsilon-connected ordinal set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
x is set
k is epsilon-transitive epsilon-connected ordinal set
m is epsilon-transitive epsilon-connected ordinal set
a +^ m is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
b +^ n is epsilon-transitive epsilon-connected ordinal set
a +^ (b +^ n) is epsilon-transitive epsilon-connected ordinal set
(a +^ b) +^ n is epsilon-transitive epsilon-connected ordinal set
(a +^ b) +^ {} is epsilon-transitive epsilon-connected ordinal set
(a +^ b) +^ {} is epsilon-transitive epsilon-connected ordinal set
b +^ {} is epsilon-transitive epsilon-connected ordinal set
a +^ (b +^ {}) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
1 *^ b is epsilon-transitive epsilon-connected ordinal set
b *^ 1 is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
b *^ 1 is epsilon-transitive epsilon-connected ordinal set
1 *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
1 *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b +^ b is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
b is set
a . b is set
a is epsilon-transitive epsilon-connected ordinal set
b . a is epsilon-transitive epsilon-connected ordinal set
a +^ (b . a) is epsilon-transitive epsilon-connected ordinal set
b . b is set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
b is set
a . b is set
a is epsilon-transitive epsilon-connected ordinal set
b . a is epsilon-transitive epsilon-connected ordinal set
(b . a) +^ a is epsilon-transitive epsilon-connected ordinal set
b . b is set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
b is set
a . b is set
a is epsilon-transitive epsilon-connected ordinal set
b . a is epsilon-transitive epsilon-connected ordinal set
a *^ (b . a) is epsilon-transitive epsilon-connected ordinal set
b . b is set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
b is set
a . b is set
a is epsilon-transitive epsilon-connected ordinal set
b . a is epsilon-transitive epsilon-connected ordinal set
(b . a) *^ a is epsilon-transitive epsilon-connected ordinal set
b . b is set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
sup b is epsilon-transitive epsilon-connected ordinal set
rng b is set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a +^ (sup a) is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal Element of dom a is epsilon-transitive epsilon-connected ordinal Element of dom a
a . the epsilon-transitive epsilon-connected ordinal Element of dom a is epsilon-transitive epsilon-connected ordinal set
a +^ (sup (rng a)) is epsilon-transitive epsilon-connected ordinal set
a is set
x is epsilon-transitive epsilon-connected ordinal set
k is epsilon-transitive epsilon-connected ordinal set
a +^ k is epsilon-transitive epsilon-connected ordinal set
m is epsilon-transitive epsilon-connected ordinal set
n is set
a . n is set
y9 is epsilon-transitive epsilon-connected ordinal set
b . y9 is epsilon-transitive epsilon-connected ordinal set
a +^ m is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
b . the epsilon-transitive epsilon-connected ordinal Element of dom a is epsilon-transitive epsilon-connected ordinal set
a is set
x is epsilon-transitive epsilon-connected ordinal set
k is epsilon-transitive epsilon-connected ordinal set
m is set
b . m is set
n is epsilon-transitive epsilon-connected ordinal set
a . n is epsilon-transitive epsilon-connected ordinal set
y9 is epsilon-transitive epsilon-connected ordinal set
a +^ y9 is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
union (sup a) is epsilon-transitive epsilon-connected ordinal set
union (sup (rng a)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
b is set
a is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
k is set
a . k is set
succ x is non empty epsilon-transitive epsilon-connected ordinal set
{x} is non empty set
x \/ {x} is non empty set
m is epsilon-transitive epsilon-connected ordinal set
succ m is non empty epsilon-transitive epsilon-connected ordinal set
{m} is non empty set
m \/ {m} is non empty set
a . (succ m) is epsilon-transitive epsilon-connected ordinal set
(succ m) *^ b is epsilon-transitive epsilon-connected ordinal set
m *^ b is epsilon-transitive epsilon-connected ordinal set
(m *^ b) +^ b is epsilon-transitive epsilon-connected ordinal set
(m *^ b) +^ (succ {}) is epsilon-transitive epsilon-connected ordinal set
(m *^ b) +^ {} is epsilon-transitive epsilon-connected ordinal set
succ ((m *^ b) +^ {}) is non empty epsilon-transitive epsilon-connected ordinal set
{((m *^ b) +^ {})} is non empty set
((m *^ b) +^ {}) \/ {((m *^ b) +^ {})} is non empty set
a . m is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
sup b is epsilon-transitive epsilon-connected ordinal set
rng b is set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
union (sup b) is epsilon-transitive epsilon-connected ordinal set
union (sup (rng b)) is epsilon-transitive epsilon-connected ordinal set
b is set
a is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
k is set
b . k is set
m is epsilon-transitive epsilon-connected ordinal set
succ m is non empty epsilon-transitive epsilon-connected ordinal set
{m} is non empty set
m \/ {m} is non empty set
n is non empty epsilon-transitive epsilon-connected ordinal set
n *^ a is epsilon-transitive epsilon-connected ordinal set
x +^ {} is epsilon-transitive epsilon-connected ordinal set
m *^ a is epsilon-transitive epsilon-connected ordinal set
(m *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set
x +^ a is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
sup b is epsilon-transitive epsilon-connected ordinal set
rng b is set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(sup a) *^ a is epsilon-transitive epsilon-connected ordinal set
(sup (rng a)) *^ a is epsilon-transitive epsilon-connected ordinal set
b is set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ a is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
k is set
a . k is set
m is epsilon-transitive epsilon-connected ordinal set
b . m is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
x *^ a is epsilon-transitive epsilon-connected ordinal set
b is set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
x is set
b . x is set
k is epsilon-transitive epsilon-connected ordinal set
a . k is epsilon-transitive epsilon-connected ordinal set
m is epsilon-transitive epsilon-connected ordinal set
m *^ a is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b,a) is T-Sequence-like Relation-like Function-like Ordinal-yielding set
sup (b,a) is epsilon-transitive epsilon-connected ordinal set
rng (b,a) is set
sup (rng (b,a)) is epsilon-transitive epsilon-connected ordinal set
b +^ (sup a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a . a is epsilon-transitive epsilon-connected ordinal set
(b,a) . a is epsilon-transitive epsilon-connected ordinal set
b +^ b is epsilon-transitive epsilon-connected ordinal set
dom (b,a) is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b,a) is T-Sequence-like Relation-like Function-like Ordinal-yielding set
sup (b,a) is epsilon-transitive epsilon-connected ordinal set
rng (b,a) is set
sup (rng (b,a)) is epsilon-transitive epsilon-connected ordinal set
(sup a) *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a . a is epsilon-transitive epsilon-connected ordinal set
(b,a) . a is epsilon-transitive epsilon-connected ordinal set
b *^ b is epsilon-transitive epsilon-connected ordinal set
dom (b,a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
union a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
union (b +^ a) is epsilon-transitive epsilon-connected ordinal set
b +^ (union a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
b +^ a is epsilon-transitive epsilon-connected ordinal set
succ (b +^ a) is non empty epsilon-transitive epsilon-connected ordinal set
{(b +^ a)} is non empty set
(b +^ a) \/ {(b +^ a)} is non empty set
union (succ (b +^ a)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a +^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
a *^ a is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
(a +^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
a +^ (succ b) is epsilon-transitive epsilon-connected ordinal set
(a +^ (succ b)) *^ a is epsilon-transitive epsilon-connected ordinal set
(succ b) *^ a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ ((succ b) *^ a) is epsilon-transitive epsilon-connected ordinal set
succ (a +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
{(a +^ b)} is non empty set
(a +^ b) \/ {(a +^ b)} is non empty set
(succ (a +^ b)) *^ a is epsilon-transitive epsilon-connected ordinal set
((a *^ a) +^ (b *^ a)) +^ a is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ ((b *^ a) +^ a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
(a +^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
(a,b) is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom (a,b) is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
x is set
k is epsilon-transitive epsilon-connected ordinal set
b . k is epsilon-transitive epsilon-connected ordinal set
a . k is epsilon-transitive epsilon-connected ordinal set
(a,b) . x is set
m is epsilon-transitive epsilon-connected ordinal set
m *^ a is epsilon-transitive epsilon-connected ordinal set
a +^ k is epsilon-transitive epsilon-connected ordinal set
(a +^ k) *^ a is epsilon-transitive epsilon-connected ordinal set
k *^ a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ (k *^ a) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ n is epsilon-transitive epsilon-connected ordinal set
((a *^ a),a) is T-Sequence-like Relation-like Function-like Ordinal-yielding set
((a *^ a),a) . x is set
a . {} is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
dom ((a *^ a),a) is epsilon-transitive epsilon-connected ordinal set
sup b is epsilon-transitive epsilon-connected ordinal set
rng b is set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
sup (a,b) is epsilon-transitive epsilon-connected ordinal set
rng (a,b) is set
sup (rng (a,b)) is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ (sup a) is epsilon-transitive epsilon-connected ordinal set
union ((a *^ a) +^ (sup a)) is epsilon-transitive epsilon-connected ordinal set
union (sup a) is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ (union (sup a)) is epsilon-transitive epsilon-connected ordinal set
a +^ {} is epsilon-transitive epsilon-connected ordinal set
(a +^ {}) *^ a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ {} is epsilon-transitive epsilon-connected ordinal set
{} *^ a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ ({} *^ a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ 1 is epsilon-transitive epsilon-connected ordinal set
a *^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
b *^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ {} is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
a is non empty epsilon-transitive epsilon-connected ordinal set
a *^ a is epsilon-transitive epsilon-connected ordinal set
x is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set
(a *^ a) +^ x is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ a is epsilon-transitive epsilon-connected ordinal set
x is non empty epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ x is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ a is epsilon-transitive epsilon-connected ordinal set
x is non empty epsilon-transitive epsilon-connected ordinal set
(a *^ a) +^ x is epsilon-transitive epsilon-connected ordinal set
k is non empty epsilon-transitive epsilon-connected ordinal set
k *^ a is epsilon-transitive epsilon-connected ordinal set
m is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set
(k *^ a) +^ m is epsilon-transitive epsilon-connected ordinal set
a is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set
a *^ a is epsilon-transitive epsilon-connected ordinal set
b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set
(a *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set
{} +^ {} is epsilon-transitive epsilon-connected ordinal natural set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
b +^ x is epsilon-transitive epsilon-connected ordinal set
x *^ a is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ (x *^ a) is epsilon-transitive epsilon-connected ordinal set
((b *^ a) +^ (x *^ a)) +^ a is epsilon-transitive epsilon-connected ordinal set
(x *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ ((x *^ a) +^ a) is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
b +^ x is epsilon-transitive epsilon-connected ordinal set
x *^ a is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ (x *^ a) is epsilon-transitive epsilon-connected ordinal set
((b *^ a) +^ (x *^ a)) +^ b is epsilon-transitive epsilon-connected ordinal set
(x *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ ((x *^ a) +^ b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
a is set
a . a is set
x is epsilon-transitive epsilon-connected ordinal set
x *^ a is epsilon-transitive epsilon-connected ordinal set
b +^ 1 is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
succ x is non empty epsilon-transitive epsilon-connected ordinal set
{x} is non empty set
x \/ {x} is non empty set
(succ x) *^ a is epsilon-transitive epsilon-connected ordinal set
(x *^ a) +^ a is epsilon-transitive epsilon-connected ordinal set
a . (succ x) is epsilon-transitive epsilon-connected ordinal set
union (sup a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
a *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
{} *^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ b is epsilon-transitive epsilon-connected ordinal set
(b *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
b *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
(succ b) *^ b is epsilon-transitive epsilon-connected ordinal set
((succ b) *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
(succ b) *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
(b *^ b) +^ b is epsilon-transitive epsilon-connected ordinal set
((b *^ b) +^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
(b *^ (b *^ a)) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
1 *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
(b *^ (b *^ a)) +^ (1 *^ (b *^ a)) is epsilon-transitive epsilon-connected ordinal set
b +^ 1 is epsilon-transitive epsilon-connected ordinal set
(b +^ 1) *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ b is epsilon-transitive epsilon-connected ordinal set
(b *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
b *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
(a,b) is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom (a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,b) . a is epsilon-transitive epsilon-connected ordinal set
a *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
b . a is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
(b . a) *^ a is epsilon-transitive epsilon-connected ordinal set
1 *^ 1 is epsilon-transitive epsilon-connected ordinal set
sup (a,b) is epsilon-transitive epsilon-connected ordinal set
rng (a,b) is set
sup (rng (a,b)) is epsilon-transitive epsilon-connected ordinal set
sup b is epsilon-transitive epsilon-connected ordinal set
rng b is set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
(b *^ b) *^ 1 is epsilon-transitive epsilon-connected ordinal set
(b *^ b) *^ {} is epsilon-transitive epsilon-connected ordinal set
b *^ 1 is epsilon-transitive epsilon-connected ordinal set
b *^ {} is epsilon-transitive epsilon-connected ordinal set
{} *^ b is epsilon-transitive epsilon-connected ordinal set
({} *^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
{} *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b +^ b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a *^ b) +^ b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(b *^ b) +^ a is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
k is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
(a,b) *^ b is epsilon-transitive epsilon-connected ordinal set
(a,((a,b) *^ b)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b,a) is epsilon-transitive epsilon-connected ordinal set
a +^ (b,a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
((a +^ b),a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
(b,a) is epsilon-transitive epsilon-connected ordinal set
a +^ (b,a) is epsilon-transitive epsilon-connected ordinal set
a +^ (a,a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
a +^ {} is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b,a) is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,{}) is epsilon-transitive epsilon-connected ordinal set
({},a) is epsilon-transitive epsilon-connected ordinal set
{} +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b +^ a is epsilon-transitive epsilon-connected ordinal set
(a,(b +^ a)) is epsilon-transitive epsilon-connected ordinal set
((a,b),a) is epsilon-transitive epsilon-connected ordinal set
(b +^ a) +^ (a,(b +^ a)) is epsilon-transitive epsilon-connected ordinal set
a +^ (a,(b +^ a)) is epsilon-transitive epsilon-connected ordinal set
b +^ (a +^ (a,(b +^ a))) is epsilon-transitive epsilon-connected ordinal set
b +^ (a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
(b,a) is epsilon-transitive epsilon-connected ordinal set
a +^ (b,a) is epsilon-transitive epsilon-connected ordinal set
b +^ (a,b) is epsilon-transitive epsilon-connected ordinal set
a +^ (a,a) is epsilon-transitive epsilon-connected ordinal set
(b,a) +^ (a,b) is epsilon-transitive epsilon-connected ordinal set
a +^ ((b,a) +^ (a,b)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
(b,a) is epsilon-transitive epsilon-connected ordinal set
a +^ (a,a) is epsilon-transitive epsilon-connected ordinal set
a +^ (b,a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a +^ a is epsilon-transitive epsilon-connected ordinal set
(b,a) is epsilon-transitive epsilon-connected ordinal set
((a +^ a),a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
((a +^ b),a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
b +^ (a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
((a *^ b),(a *^ b)) is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
(a,a) *^ b is epsilon-transitive epsilon-connected ordinal set
{} *^ b is epsilon-transitive epsilon-connected ordinal set
a *^ {} is epsilon-transitive epsilon-connected ordinal set
a +^ (a,a) is epsilon-transitive epsilon-connected ordinal set
(a *^ b) +^ ((a,a) *^ b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
(a,b) *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
((a,b) *^ b) +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
(a,b) *^ b is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
(a,((a,b) *^ b)) is epsilon-transitive epsilon-connected ordinal set
((a,b) *^ b) +^ (a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
(a,a) *^ a is epsilon-transitive epsilon-connected ordinal set
(a,((a,a) *^ a)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
(a,a) *^ a is epsilon-transitive epsilon-connected ordinal set
(a,((a,a) *^ a)) is epsilon-transitive epsilon-connected ordinal set
((a,a) *^ a) +^ (a,a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
((a,a) *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
((a,a) *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b *^ a is epsilon-transitive epsilon-connected ordinal set
((b *^ a),a) is epsilon-transitive epsilon-connected ordinal set
(b *^ a) +^ {} is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
((a *^ b),b) is epsilon-transitive epsilon-connected ordinal set
((a *^ b),b) is epsilon-transitive epsilon-connected ordinal set
((a *^ b),b) *^ b is epsilon-transitive epsilon-connected ordinal set
((a *^ b),(((a *^ b),b) *^ b)) is epsilon-transitive epsilon-connected ordinal set
a *^ {} is epsilon-transitive epsilon-connected ordinal set
((a *^ b),(a *^ b)) is epsilon-transitive epsilon-connected ordinal set
({},(((a *^ b),b) *^ b)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
({},a) is epsilon-transitive epsilon-connected ordinal set
({},a) is epsilon-transitive epsilon-connected ordinal set
({},a) *^ a is epsilon-transitive epsilon-connected ordinal set
({},(({},a) *^ a)) is epsilon-transitive epsilon-connected ordinal set
(a,{}) is epsilon-transitive epsilon-connected ordinal set
(a,{}) is epsilon-transitive epsilon-connected ordinal set
(a,{}) *^ {} is epsilon-transitive epsilon-connected ordinal set
(a,((a,{}) *^ {})) is epsilon-transitive epsilon-connected ordinal set
{} *^ a is epsilon-transitive epsilon-connected ordinal set
(a,{}) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,1) is epsilon-transitive epsilon-connected ordinal set
(a,1) is epsilon-transitive epsilon-connected ordinal set
(a,1) *^ 1 is epsilon-transitive epsilon-connected ordinal set
(a,((a,1) *^ 1)) is epsilon-transitive epsilon-connected ordinal set
a *^ 1 is epsilon-transitive epsilon-connected ordinal set
a +^ {} is epsilon-transitive epsilon-connected ordinal set
(a,a) is epsilon-transitive epsilon-connected ordinal set
a is set
sup a is epsilon-transitive epsilon-connected ordinal set
On a is set
union (On a) is set
succ (union (On a)) is non empty set
{(union (On a))} is non empty set
(union (On a)) \/ {(union (On a))} is non empty set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
a is set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
b is T-Sequence-like Relation-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
rng b is set
sup b is epsilon-transitive epsilon-connected ordinal set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
a is set
b is set
b . b is set
b is epsilon-transitive epsilon-connected ordinal set
b . b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b . a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b . b is epsilon-transitive epsilon-connected ordinal set
b . {} is epsilon-transitive epsilon-connected ordinal set
{(b . {})} is non empty set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a +^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural set
b is epsilon-transitive epsilon-connected ordinal natural set
(a,b) is epsilon-transitive epsilon-connected ordinal set
b +^ (a,b) is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural set
a *^ b is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal natural set
{a} is non empty set
a \/ {a} is non empty set
(succ a) *^ b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural set
b +^ b is epsilon-transitive epsilon-connected ordinal natural set
{} *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a *^ b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural set
b is epsilon-transitive epsilon-connected ordinal natural set
a +^ b is epsilon-transitive epsilon-connected ordinal natural set
b +^ a is epsilon-transitive epsilon-connected ordinal natural set
b is epsilon-transitive epsilon-connected ordinal natural set
a +^ b is epsilon-transitive epsilon-connected ordinal natural set
b +^ a is epsilon-transitive epsilon-connected ordinal natural set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural set
{b} is non empty set
b \/ {b} is non empty set
a is epsilon-transitive epsilon-connected ordinal natural set
(succ b) +^ a is epsilon-transitive epsilon-connected ordinal natural set
b +^ a is epsilon-transitive epsilon-connected ordinal natural set
succ (b +^ a) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(b +^ a)} is non empty set
(b +^ a) \/ {(b +^ a)} is non empty set
succ a is non empty epsilon-transitive epsilon-connected ordinal natural set
{a} is non empty set
a \/ {a} is non empty set
(succ b) +^ (succ a) is epsilon-transitive epsilon-connected ordinal natural set
succ ((succ b) +^ a) is non empty epsilon-transitive epsilon-connected ordinal natural set
{((succ b) +^ a)} is non empty set
((succ b) +^ a) \/ {((succ b) +^ a)} is non empty set
b +^ (succ a) is epsilon-transitive epsilon-connected ordinal natural set
succ (b +^ (succ a)) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(b +^ (succ a))} is non empty set
(b +^ (succ a)) \/ {(b +^ (succ a))} is non empty set
(succ b) +^ {} is epsilon-transitive epsilon-connected ordinal natural set
b +^ {} is epsilon-transitive epsilon-connected ordinal natural set
succ (b +^ {}) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(b +^ {})} is non empty set
(b +^ {}) \/ {(b +^ {})} is non empty set
(succ b) +^ a is epsilon-transitive epsilon-connected ordinal natural set
succ (b +^ a) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(b +^ a)} is non empty set
(b +^ a) \/ {(b +^ a)} is non empty set
a +^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set
a +^ {} is epsilon-transitive epsilon-connected ordinal natural set
{} +^ a is epsilon-transitive epsilon-connected ordinal natural set
a is epsilon-transitive epsilon-connected ordinal natural set
b is epsilon-transitive epsilon-connected ordinal natural set
a *^ b is epsilon-transitive epsilon-connected ordinal natural set
b *^ a is epsilon-transitive epsilon-connected ordinal natural set
b is epsilon-transitive epsilon-connected ordinal natural set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural set
{b} is non empty set
b \/ {b} is non empty set
a *^ b is epsilon-transitive epsilon-connected ordinal natural set
b *^ a is epsilon-transitive epsilon-connected ordinal natural set
a is epsilon-transitive epsilon-connected ordinal natural set
a *^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set
a *^ b is epsilon-transitive epsilon-connected ordinal natural set
((a *^ b),a) is epsilon-transitive epsilon-connected ordinal natural set
succ a is non empty epsilon-transitive epsilon-connected ordinal natural set
{a} is non empty set
a \/ {a} is non empty set
(succ a) *^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set
((a *^ (succ b)),(succ b)) is epsilon-transitive epsilon-connected ordinal natural set
(a,(succ b)) is epsilon-transitive epsilon-connected ordinal natural set
((a *^ b),(a,(succ b))) is epsilon-transitive epsilon-connected ordinal natural set
(a,b) is epsilon-transitive epsilon-connected ordinal natural set
succ (a,b) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(a,b)} is non empty set
(a,b) \/ {(a,b)} is non empty set
((a *^ b),(succ (a,b))) is epsilon-transitive epsilon-connected ordinal natural set
((a *^ b),(a,b)) is epsilon-transitive epsilon-connected ordinal natural set
succ ((a *^ b),(a,b)) is non empty epsilon-transitive epsilon-connected ordinal natural set
{((a *^ b),(a,b))} is non empty set
((a *^ b),(a,b)) \/ {((a *^ b),(a,b))} is non empty set
((a *^ b),b) is epsilon-transitive epsilon-connected ordinal natural set
(((a *^ b),b),a) is epsilon-transitive epsilon-connected ordinal natural set
succ (((a *^ b),b),a) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(((a *^ b),b),a)} is non empty set
(((a *^ b),b),a) \/ {(((a *^ b),b),a)} is non empty set
(succ a) *^ b is epsilon-transitive epsilon-connected ordinal natural set
(((succ a) *^ b),a) is epsilon-transitive epsilon-connected ordinal natural set
succ (((succ a) *^ b),a) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(((succ a) *^ b),a)} is non empty set
(((succ a) *^ b),a) \/ {(((succ a) *^ b),a)} is non empty set
(((succ a) *^ b),(succ a)) is epsilon-transitive epsilon-connected ordinal natural set
{} *^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set
({},{}) is epsilon-transitive epsilon-connected ordinal natural set
{} *^ b is epsilon-transitive epsilon-connected ordinal natural set
(({} *^ b),{}) is epsilon-transitive epsilon-connected ordinal natural set
a *^ (succ b) is epsilon-transitive epsilon-connected ordinal natural set
((a *^ b),a) is epsilon-transitive epsilon-connected ordinal natural set
(succ b) *^ a is epsilon-transitive epsilon-connected ordinal natural set
a *^ {} is epsilon-transitive epsilon-connected ordinal natural set
{} *^ a is epsilon-transitive epsilon-connected ordinal natural set