:: NECKLACE semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

COMPLEX is set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool omega is non empty non trivial non finite set

{} is set

the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V23() V24() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element Function-yielding V102() set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V23() V24() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element Function-yielding V102() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT

{{},1} is finite set

bool NAT is non empty non trivial non finite set

0 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

4 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT

{{}} is non empty trivial finite 1 -element set

{{},1,2,3} is non empty finite set

{0,1,2,3} is non empty finite set

n is set

S is set

T is set

{n,S,T} is non empty finite set

x is set

[n,x] is non empty set

{n,x} is finite set

{n} is non empty trivial finite 1 -element set

{{n,x},{n}} is finite V39() set

[S,x] is non empty set

{S,x} is finite set

{S} is non empty trivial finite 1 -element set

{{S,x},{S}} is finite V39() set

[T,x] is non empty set

{T,x} is finite set

{T} is non empty trivial finite 1 -element set

{{T,x},{T}} is finite V39() set

i is set

[n,i] is non empty set

{n,i} is finite set

{{n,i},{n}} is finite V39() set

[S,i] is non empty set

{S,i} is finite set

{{S,i},{S}} is finite V39() set

[T,i] is non empty set

{T,i} is finite set

{{T,i},{T}} is finite V39() set

x1 is set

{x,i,x1} is non empty finite set

[:{n,S,T},{x,i,x1}:] is Relation-like non empty finite set

[n,x1] is non empty set

{n,x1} is finite set

{{n,x1},{n}} is finite V39() set

[S,x1] is non empty set

{S,x1} is finite set

{{S,x1},{S}} is finite V39() set

[T,x1] is non empty set

{T,x1} is finite set

{{T,x1},{T}} is finite V39() set

{[n,x],[n,i],[n,x1],[S,x],[S,i],[S,x1],[T,x],[T,i],[T,x1]} is non empty set

{S,T} is finite set

{n} \/ {S,T} is finite set

[:({n} \/ {S,T}),{x,i,x1}:] is Relation-like finite set

{x} is non empty trivial finite 1 -element set

{i,x1} is finite set

{x} \/ {i,x1} is finite set

[:({n} \/ {S,T}),({x} \/ {i,x1}):] is Relation-like finite set

[:{n},{x}:] is Relation-like non empty finite set

[:{n},{i,x1}:] is Relation-like finite set

[:{n},{x}:] \/ [:{n},{i,x1}:] is Relation-like finite set

[:{S,T},{x}:] is Relation-like finite set

([:{n},{x}:] \/ [:{n},{i,x1}:]) \/ [:{S,T},{x}:] is Relation-like finite set

[:{S,T},{i,x1}:] is Relation-like finite set

(([:{n},{x}:] \/ [:{n},{i,x1}:]) \/ [:{S,T},{x}:]) \/ [:{S,T},{i,x1}:] is Relation-like finite set

[:{S},{i,x1}:] is Relation-like finite set

[:{T},{i,x1}:] is Relation-like finite set

[:{S},{i,x1}:] \/ [:{T},{i,x1}:] is Relation-like finite set

(([:{n},{x}:] \/ [:{n},{i,x1}:]) \/ [:{S,T},{x}:]) \/ ([:{S},{i,x1}:] \/ [:{T},{i,x1}:]) is Relation-like finite set

{[n,x]} is Relation-like Function-like constant non empty trivial finite 1 -element set

{[n,x]} \/ [:{n},{i,x1}:] is Relation-like finite set

({[n,x]} \/ [:{n},{i,x1}:]) \/ [:{S,T},{x}:] is Relation-like finite set

(({[n,x]} \/ [:{n},{i,x1}:]) \/ [:{S,T},{x}:]) \/ ([:{S},{i,x1}:] \/ [:{T},{i,x1}:]) is Relation-like finite set

{[n,i],[n,x1]} is Relation-like finite set

{[n,x]} \/ {[n,i],[n,x1]} is Relation-like finite set

({[n,x]} \/ {[n,i],[n,x1]}) \/ [:{S,T},{x}:] is Relation-like finite set

(({[n,x]} \/ {[n,i],[n,x1]}) \/ [:{S,T},{x}:]) \/ ([:{S},{i,x1}:] \/ [:{T},{i,x1}:]) is Relation-like finite set

{[S,x],[T,x]} is Relation-like finite set

({[n,x]} \/ {[n,i],[n,x1]}) \/ {[S,x],[T,x]} is Relation-like finite set

(({[n,x]} \/ {[n,i],[n,x1]}) \/ {[S,x],[T,x]}) \/ ([:{S},{i,x1}:] \/ [:{T},{i,x1}:]) is Relation-like finite set

{[S,i],[S,x1]} is Relation-like finite set

{[S,i],[S,x1]} \/ [:{T},{i,x1}:] is Relation-like finite set

(({[n,x]} \/ {[n,i],[n,x1]}) \/ {[S,x],[T,x]}) \/ ({[S,i],[S,x1]} \/ [:{T},{i,x1}:]) is Relation-like finite set

{[T,i],[T,x1]} is Relation-like finite set

{[S,i],[S,x1]} \/ {[T,i],[T,x1]} is Relation-like finite set

(({[n,x]} \/ {[n,i],[n,x1]}) \/ {[S,x],[T,x]}) \/ ({[S,i],[S,x1]} \/ {[T,i],[T,x1]}) is Relation-like finite set

{[n,x],[n,i],[n,x1]} is non empty finite set

{[n,x],[n,i],[n,x1]} \/ {[S,x],[T,x]} is finite set

({[n,x],[n,i],[n,x1]} \/ {[S,x],[T,x]}) \/ ({[S,i],[S,x1]} \/ {[T,i],[T,x1]}) is finite set

{[n,x],[n,i],[n,x1],[S,x],[T,x]} is non empty finite set

{[n,x],[n,i],[n,x1],[S,x],[T,x]} \/ ({[S,i],[S,x1]} \/ {[T,i],[T,x1]}) is finite set

{[S,i],[S,x1],[T,i],[T,x1]} is non empty finite set

{[n,x],[n,i],[n,x1],[S,x],[T,x]} \/ {[S,i],[S,x1],[T,i],[T,x1]} is finite set

{[n,x],[n,i],[n,x1],[S,x],[T,x],[S,i],[S,x1],[T,i],[T,x1]} is non empty set

{[n,x],[n,i],[n,x1],[S,x]} is non empty finite set

{[T,x],[S,i],[S,x1],[T,i],[T,x1]} is non empty finite set

{[n,x],[n,i],[n,x1],[S,x]} \/ {[T,x],[S,i],[S,x1],[T,i],[T,x1]} is finite set

{[T,x],[S,i],[S,x1]} is non empty finite set

{[T,x],[S,i],[S,x1]} \/ {[T,i],[T,x1]} is finite set

{[n,x],[n,i],[n,x1],[S,x]} \/ ({[T,x],[S,i],[S,x1]} \/ {[T,i],[T,x1]}) is finite set

{[S,i],[S,x1],[T,x]} is non empty finite set

{[S,i],[S,x1],[T,x]} \/ {[T,i],[T,x1]} is finite set

{[n,x],[n,i],[n,x1],[S,x]} \/ ({[S,i],[S,x1],[T,x]} \/ {[T,i],[T,x1]}) is finite set

{[S,i],[S,x1],[T,x],[T,i],[T,x1]} is non empty finite set

{[n,x],[n,i],[n,x1],[S,x]} \/ {[S,i],[S,x1],[T,x],[T,i],[T,x1]} is finite set

n is set

S is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

T is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

{ b

x is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

n is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

S is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

{ b

n is set

delta n is Relation-like n -defined [:n,n:] -valued Function-like quasi_total Element of bool [:n,[:n,n:]:]

[:n,n:] is Relation-like set

[:n,[:n,n:]:] is Relation-like set

bool [:n,[:n,n:]:] is non empty set

T is set

dom (delta n) is set

x is set

(delta n) . T is set

(delta n) . x is set

dom (delta n) is Element of bool n

bool n is non empty set

[T,T] is non empty set

{T,T} is finite set

{T} is non empty trivial finite 1 -element set

{{T,T},{T}} is finite V39() set

[x,x] is non empty set

{x,x} is finite set

{x} is non empty trivial finite 1 -element set

{{x,x},{x}} is finite V39() set

n is set

id n is Relation-like n -defined n -valued Function-like one-to-one V28(n) quasi_total Element of bool [:n,n:]

[:n,n:] is Relation-like set

bool [:n,n:] is non empty set

card (id n) is epsilon-transitive epsilon-connected ordinal cardinal set

card n is epsilon-transitive epsilon-connected ordinal cardinal set

Funcs (n,n) is functional non empty set

n is Relation-like Function-like set

S is set

dom n is set

T is set

n . S is set

n . T is set

x is Relation-like Function-like constant trivial finite set

dom x is trivial finite set

i is set

{i} is non empty trivial finite 1 -element set

n is Relation-like Function-like set

dom n is set

S is Relation-like Function-like set

dom S is set

n +* S is Relation-like Function-like set

rng (n +* S) is set

rng n is set

rng S is set

(rng n) \/ (rng S) is set

n is Relation-like Function-like one-to-one set

dom n is set

S is Relation-like Function-like one-to-one set

dom S is set

rng n is set

rng S is set

n +* S is Relation-like Function-like set

(n +* S) " is Relation-like Function-like set

n " is Relation-like Function-like one-to-one set

S " is Relation-like Function-like one-to-one set

(n ") +* (S ") is Relation-like Function-like set

rng (n +* S) is set

dom (n +* S) is set

T is set

x is set

((n ") +* (S ")) . T is set

(n +* S) . x is set

(rng n) \/ (rng S) is set

i is set

n . i is set

(dom n) \/ (dom S) is set

dom (n ") is set

dom (S ") is set

(n +* S) . i is set

(n ") . T is set

dom (n ") is set

dom (S ") is set

i is set

S . i is set

(S ") . T is set

(S ") +* (n ") is Relation-like Function-like set

((S ") +* (n ")) . T is set

(dom n) \/ (dom S) is set

S +* n is Relation-like Function-like set

(S +* n) . i is set

(dom n) \/ (dom S) is set

n . x is set

(n ") . T is set

dom (n ") is set

dom (S ") is set

(rng n) \/ (rng S) is set

S . x is set

(rng n) \/ (rng S) is set

dom (n ") is set

dom (S ") is set

(S ") . T is set

(S ") +* (n ") is Relation-like Function-like set

((S ") +* (n ")) . T is set

dom ((n ") +* (S ")) is set

dom (n ") is set

dom (S ") is set

(dom (n ")) \/ (dom (S ")) is set

(rng n) \/ (dom (S ")) is set

(rng n) \/ (rng S) is set

n is set

S is set

n --> S is Relation-like n -defined {S} -valued Function-like constant V28(n) quasi_total Element of bool [:n,{S}:]

{S} is non empty trivial finite 1 -element set

[:n,{S}:] is Relation-like set

bool [:n,{S}:] is non empty set

T is set

n --> T is Relation-like n -defined {T} -valued Function-like constant V28(n) quasi_total Element of bool [:n,{T}:]

{T} is non empty trivial finite 1 -element set

[:n,{T}:] is Relation-like set

bool [:n,{T}:] is non empty set

(n --> S) +* (n --> T) is Relation-like n -defined Function-like V28(n) set

dom (n --> T) is Element of bool n

bool n is non empty set

dom (n --> S) is Element of bool n

n is set

S is set

n .--> S is Relation-like {n} -defined Function-like one-to-one constant trivial finite set

{n} is non empty trivial finite 1 -element set

{n} --> S is Relation-like {n} -defined {S} -valued Function-like constant non empty V28({n}) quasi_total finite Element of bool [:{n},{S}:]

{S} is non empty trivial finite 1 -element set

[:{n},{S}:] is Relation-like non empty finite set

bool [:{n},{S}:] is non empty finite V39() set

(n .--> S) " is Relation-like Function-like one-to-one set

S .--> n is Relation-like {S} -defined Function-like one-to-one constant trivial finite set

{S} --> n is Relation-like {S} -defined {n} -valued Function-like constant non empty V28({S}) quasi_total finite Element of bool [:{S},{n}:]

[:{S},{n}:] is Relation-like non empty finite set

bool [:{S},{n}:] is non empty finite V39() set

rng (n .--> S) is trivial finite set

dom (n .--> S) is trivial finite Element of bool {n}

bool {n} is non empty finite V39() set

i is set

x1 is set

(S .--> n) . i is set

(n .--> S) . x1 is set

(S .--> n) . S is set

(n .--> S) . n is set

dom (S .--> n) is trivial finite Element of bool {S}

bool {S} is non empty finite V39() set

n is set

S is set

T is set

x is set

(n,S) --> (T,x) is Relation-like Function-like finite set

((n,S) --> (T,x)) " is Relation-like Function-like set

(T,x) --> (n,S) is Relation-like Function-like finite set

(n,n) --> (x,x) is Relation-like Function-like finite set

((n,n) --> (x,x)) " is Relation-like Function-like set

n .--> x is Relation-like {n} -defined Function-like one-to-one constant trivial finite set

{n} is non empty trivial finite 1 -element set

{n} --> x is Relation-like {n} -defined {x} -valued Function-like constant non empty V28({n}) quasi_total finite Element of bool [:{n},{x}:]

{x} is non empty trivial finite 1 -element set

[:{n},{x}:] is Relation-like non empty finite set

bool [:{n},{x}:] is non empty finite V39() set

(n .--> x) " is Relation-like Function-like one-to-one set

x .--> n is Relation-like {x} -defined Function-like one-to-one constant trivial finite set

{x} --> n is Relation-like {x} -defined {n} -valued Function-like constant non empty V28({x}) quasi_total finite Element of bool [:{x},{n}:]

[:{x},{n}:] is Relation-like non empty finite set

bool [:{x},{n}:] is non empty finite V39() set

(x,x) --> (n,n) is Relation-like Function-like finite set

rng ((n,S) --> (T,x)) is finite set

dom ((n,S) --> (T,x)) is finite set

x2 is set

B is set

((T,x) --> (n,S)) . x2 is set

((n,S) --> (T,x)) . B is set

{n,S} is finite set

{T,x} is finite set

{T,x} is finite set

{T,x} is finite set

{n,S} is finite set

{n,S} is finite set

{n,S} is finite set

x2 is set

B is set

((n,S) --> (T,x)) . x2 is set

((n,S) --> (T,x)) . B is set

dom ((T,x) --> (n,S)) is finite set

{T,x} is finite set

F

F

{ [F

F

{ [F

S is set

T is Element of F

F

F

[F

{F

{F

{{F

S is Relation-like set

x is set

T is set

[x,T] is non empty set

{x,T} is finite set

{x} is non empty trivial finite 1 -element set

{{x,T},{x}} is finite V39() set

[T,x] is non empty set

{T,x} is finite set

{T} is non empty trivial finite 1 -element set

{{T,x},{T}} is finite V39() set

i is Element of F

F

F

[F

{F

{F

{{F

T is set

x is set

[T,x] is non empty set

{T,x} is finite set

{T} is non empty trivial finite 1 -element set

{{T,x},{T}} is finite V39() set

[x,T] is non empty set

{x,T} is finite set

{x} is non empty trivial finite 1 -element set

{{x,T},{x}} is finite V39() set

i is Element of F

F

F

[F

{F

{F

{{F

S is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

T is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

T is non empty RelStr

the carrier of T is non empty set

id the carrier of T is Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one non empty V28( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is Relation-like non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

i is Relation-like the carrier of T -defined the carrier of T -valued Function-like non empty V28( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of T:]

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

x1 is Element of the carrier of T

x2 is Element of the carrier of T

[x1,x2] is non empty set

{x1,x2} is finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is finite V39() set

i . x1 is set

i . x2 is set

[(i . x1),(i . x2)] is non empty set

{(i . x1),(i . x2)} is finite set

{(i . x1)} is non empty trivial finite 1 -element set

{{(i . x1),(i . x2)},{(i . x1)}} is finite V39() set

i . x1 is Element of the carrier of T

S is non empty RelStr

n is non empty RelStr

T is non empty RelStr

the carrier of S is non empty set

the carrier of n is non empty set

[: the carrier of S, the carrier of n:] is Relation-like non empty set

bool [: the carrier of S, the carrier of n:] is non empty set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is Relation-like non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

[: the carrier of n, the carrier of n:] is Relation-like non empty set

bool [: the carrier of n, the carrier of n:] is non empty set

x is Relation-like the carrier of S -defined the carrier of n -valued Function-like non empty V28( the carrier of S) quasi_total Element of bool [: the carrier of S, the carrier of n:]

the carrier of T is non empty set

[: the carrier of T, the carrier of S:] is Relation-like non empty set

bool [: the carrier of T, the carrier of S:] is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is Relation-like non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

i is Relation-like the carrier of T -defined the carrier of S -valued Function-like non empty V28( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of S:]

[: the carrier of T, the carrier of n:] is Relation-like non empty set

bool [: the carrier of T, the carrier of n:] is non empty set

x * i is Relation-like the carrier of T -defined the carrier of n -valued Function-like non empty V28( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of n:]

x1 is Relation-like the carrier of T -defined the carrier of n -valued Function-like non empty V28( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of n:]

x2 is Element of the carrier of T

B is Element of the carrier of T

[x2,B] is non empty set

{x2,B} is finite set

{x2} is non empty trivial finite 1 -element set

{{x2,B},{x2}} is finite V39() set

x1 . x2 is Element of the carrier of n

x1 . B is Element of the carrier of n

[(x1 . x2),(x1 . B)] is non empty set

{(x1 . x2),(x1 . B)} is finite set

{(x1 . x2)} is non empty trivial finite 1 -element set

{{(x1 . x2),(x1 . B)},{(x1 . x2)}} is finite V39() set

i . x2 is Element of the carrier of S

i . B is Element of the carrier of S

[(i . x2),(i . B)] is non empty set

{(i . x2),(i . B)} is finite set

{(i . x2)} is non empty trivial finite 1 -element set

{{(i . x2),(i . B)},{(i . x2)}} is finite V39() set

x . (i . x2) is Element of the carrier of n

x . (i . B) is Element of the carrier of n

i . x2 is Element of the carrier of S

x . (i . x2) is Element of the carrier of n

i . B is Element of the carrier of S

x . (i . B) is Element of the carrier of n

[(i . x2),(i . B)] is non empty set

{(i . x2),(i . B)} is finite set

{(i . x2)} is non empty trivial finite 1 -element set

{{(i . x2),(i . B)},{(i . x2)}} is finite V39() set

T is non empty RelStr

x is non empty RelStr

x is non empty RelStr

T is non empty RelStr

n is non empty RelStr

S is non empty RelStr

T is non empty RelStr

n is RelStr

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

the carrier of n is set

[: the carrier of n, the carrier of n:] is Relation-like set

bool [: the carrier of n, the carrier of n:] is non empty set

the InternalRel of n ~ is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

field the InternalRel of n is set

dom the InternalRel of n is set

rng the InternalRel of n is set

(dom the InternalRel of n) \/ (rng the InternalRel of n) is set

S is set

T is set

x is set

[T,x] is non empty set

{T,x} is finite set

{T} is non empty trivial finite 1 -element set

{{T,x},{T}} is finite V39() set

[x,T] is non empty set

{x,T} is finite set

{x} is non empty trivial finite 1 -element set

{{x,T},{x}} is finite V39() set

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

{ [b

[:n,n:] is Relation-like finite set

T is set

x is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

x + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[x,(x + 1)] is non empty set

{x,(x + 1)} is finite V39() set

{x} is non empty trivial finite V39() 1 -element set

{{x,(x + 1)},{x}} is finite V39() set

bool [:n,n:] is non empty finite V39() set

T is Relation-like n -defined n -valued finite Element of bool [:n,n:]

RelStr(# n,T #) is strict RelStr

the carrier of RelStr(# n,T #) is set

the InternalRel of RelStr(# n,T #) is Relation-like the carrier of RelStr(# n,T #) -defined the carrier of RelStr(# n,T #) -valued Element of bool [: the carrier of RelStr(# n,T #), the carrier of RelStr(# n,T #):]

[: the carrier of RelStr(# n,T #), the carrier of RelStr(# n,T #):] is Relation-like set

bool [: the carrier of RelStr(# n,T #), the carrier of RelStr(# n,T #):] is non empty set

S is strict RelStr

the carrier of S is set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

T is strict RelStr

the carrier of T is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict RelStr

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]

the carrier of (n) is set

[: the carrier of (n), the carrier of (n):] is Relation-like set

bool [: the carrier of (n), the carrier of (n):] is non empty set

field the InternalRel of (n) is set

dom the InternalRel of (n) is set

rng the InternalRel of (n) is set

(dom the InternalRel of (n)) \/ (rng the InternalRel of (n)) is set

T is set

x is set

[T,x] is non empty set

{T,x} is finite set

{T} is non empty trivial finite 1 -element set

{{T,x},{T}} is finite V39() set

[x,T] is non empty set

{x,T} is finite set

{x} is non empty trivial finite 1 -element set

{{x,T},{x}} is finite V39() set

{ [b

i is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

i + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[i,(i + 1)] is non empty set

{i,(i + 1)} is finite V39() set

{i} is non empty trivial finite V39() 1 -element set

{{i,(i + 1)},{i}} is finite V39() set

x1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

x1 + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[x1,(x1 + 1)] is non empty set

{x1,(x1 + 1)} is finite V39() set

{x1} is non empty trivial finite V39() 1 -element set

{{x1,(x1 + 1)},{x1}} is finite V39() set

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict RelStr

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]

the carrier of (n) is set

[: the carrier of (n), the carrier of (n):] is Relation-like set

bool [: the carrier of (n), the carrier of (n):] is non empty set

card the InternalRel of (n) is epsilon-transitive epsilon-connected ordinal cardinal set

n - 1 is V23() V24() ext-real Element of REAL

n -' 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real non negative finite cardinal Element of NAT

0 + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

S is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

S + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

S is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

S + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

{ H

{ H

S is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

S + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[S,(S + 1)] is non empty set

{S,(S + 1)} is finite V39() set

{S} is non empty trivial finite V39() 1 -element set

{{S,(S + 1)},{S}} is finite V39() set

T is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

T + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[T,(T + 1)] is non empty set

{T,(T + 1)} is finite V39() set

{T} is non empty trivial finite V39() 1 -element set

{{T,(T + 1)},{T}} is finite V39() set

{ H

{ [b

card { [b

card (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega

n is RelStr

the carrier of n is set

[: the carrier of n, the carrier of n:] is Relation-like set

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

bool [: the carrier of n, the carrier of n:] is non empty set

the InternalRel of n ~ is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

the InternalRel of n \/ ( the InternalRel of n ~) is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #) is strict RelStr

the carrier of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #) is set

the InternalRel of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #) is Relation-like the carrier of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #) -defined the carrier of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #) -valued Element of bool [: the carrier of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #), the carrier of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #):]

[: the carrier of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #), the carrier of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #):] is Relation-like set

bool [: the carrier of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #), the carrier of RelStr(# the carrier of n,( the InternalRel of n \/ ( the InternalRel of n ~)) #):] is non empty set

S is strict RelStr

the carrier of S is set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

T is strict RelStr

the carrier of T is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

n is RelStr

(n) is strict RelStr

S is set

the carrier of (n) is set

T is set

[S,T] is non empty set

{S,T} is finite set

{S} is non empty trivial finite 1 -element set

{{S,T},{S}} is finite V39() set

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]

[: the carrier of (n), the carrier of (n):] is Relation-like set

bool [: the carrier of (n), the carrier of (n):] is non empty set

[T,S] is non empty set

{T,S} is finite set

{T} is non empty trivial finite 1 -element set

{{T,S},{T}} is finite V39() set

the carrier of n is set

[: the carrier of n, the carrier of n:] is Relation-like set

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

bool [: the carrier of n, the carrier of n:] is non empty set

the InternalRel of n ~ is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

the InternalRel of n \/ ( the InternalRel of n ~) is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

[0,0] is non empty set

{0,0} is finite V39() set

{0} is non empty trivial finite V39() 1 -element set

{{0,0},{0}} is finite V39() set

{[0,0]} is Relation-like Function-like one-to-one constant non empty trivial finite 1 -element set

[:{0},{0}:] is Relation-like non empty finite set

bool [:{0},{0}:] is non empty finite V39() set

S is Relation-like {0} -defined {0} -valued finite Element of bool [:{0},{0}:]

RelStr(# {0},S #) is non empty strict RelStr

T is non empty strict RelStr

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

the carrier of T is non empty set

[: the carrier of T, the carrier of T:] is Relation-like non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

x is set

i is set

[x,i] is non empty set

{x,i} is finite set

{x} is non empty trivial finite 1 -element set

{{x,i},{x}} is finite V39() set

[i,x] is non empty set

{i,x} is finite set

{i} is non empty trivial finite 1 -element set

{{i,x},{i}} is finite V39() set

n is () RelStr

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

the carrier of n is set

[: the carrier of n, the carrier of n:] is Relation-like set

bool [: the carrier of n, the carrier of n:] is non empty set

S is set

field the InternalRel of n is set

dom the InternalRel of n is set

rng the InternalRel of n is set

(dom the InternalRel of n) \/ (rng the InternalRel of n) is set

T is set

[S,T] is non empty set

{S,T} is finite set

{S} is non empty trivial finite 1 -element set

{{S,T},{S}} is finite V39() set

[T,S] is non empty set

{T,S} is finite set

{T} is non empty trivial finite 1 -element set

{{T,S},{T}} is finite V39() set

the carrier of n \/ the carrier of n is set

n is non empty RelStr

S is non empty RelStr

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

the carrier of n is non empty set

[: the carrier of n, the carrier of n:] is Relation-like non empty set

bool [: the carrier of n, the carrier of n:] is non empty set

card the InternalRel of n is epsilon-transitive epsilon-connected ordinal cardinal set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

the carrier of S is non empty set

[: the carrier of S, the carrier of S:] is Relation-like non empty set

bool [: the carrier of S, the carrier of S:] is non empty set

card the InternalRel of S is epsilon-transitive epsilon-connected ordinal cardinal set

[: the carrier of n, the carrier of S:] is Relation-like non empty set

bool [: the carrier of n, the carrier of S:] is non empty set

B is Relation-like the carrier of n -defined the carrier of S -valued Function-like non empty V28( the carrier of n) quasi_total Element of bool [: the carrier of n, the carrier of S:]

F is Relation-like Function-like one-to-one set

[:F,F:] is Relation-like Function-like one-to-one set

dom B is non empty Element of bool the carrier of n

bool the carrier of n is non empty set

rng B is non empty set

[:B,B:] is Relation-like [: the carrier of n, the carrier of n:] -defined [: the carrier of S, the carrier of S:] -valued Function-like non empty V28([: the carrier of n, the carrier of n:]) quasi_total Element of bool [:[: the carrier of n, the carrier of n:],[: the carrier of S, the carrier of S:]:]

[:[: the carrier of n, the carrier of n:],[: the carrier of S, the carrier of S:]:] is Relation-like non empty set

bool [:[: the carrier of n, the carrier of n:],[: the carrier of S, the carrier of S:]:] is non empty set

x2 is set

[:B,B:] | x2 is Relation-like [: the carrier of n, the carrier of n:] -defined x2 -defined [: the carrier of n, the carrier of n:] -defined [: the carrier of S, the carrier of S:] -valued Function-like Element of bool [:[: the carrier of n, the carrier of n:],[: the carrier of S, the carrier of S:]:]

dom ([:B,B:] | x2) is Relation-like Element of bool x2

bool x2 is non empty set

dom [:B,B:] is Relation-like the carrier of n -defined the carrier of n -valued non empty Element of bool [: the carrier of n, the carrier of n:]

(dom [:B,B:]) /\ x2 is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

[:(dom B),(dom B):] is Relation-like non empty set

[:(dom B),(dom B):] /\ x2 is Relation-like set

rng ([:B,B:] | x2) is Relation-like set

j is set

a is set

([:B,B:] | x2) . a is set

b is set

x1 is set

[b,x1] is non empty set

{b,x1} is finite set

{b} is non empty trivial finite 1 -element set

{{b,x1},{b}} is finite V39() set

x2 is Element of the carrier of n

x19 is Element of the carrier of n

B . x2 is Element of the carrier of S

B . x19 is Element of the carrier of S

[:B,B:] . (b,x1) is set

[:B,B:] . [b,x1] is set

B . b is set

B . x1 is set

[(B . b),(B . x1)] is non empty set

{(B . b),(B . x1)} is finite set

{(B . b)} is non empty trivial finite 1 -element set

{{(B . b),(B . x1)},{(B . b)}} is finite V39() set

[:(dom ([:B,B:] | x2)),[: the carrier of S, the carrier of S:]:] is Relation-like set

bool [:(dom ([:B,B:] | x2)),[: the carrier of S, the carrier of S:]:] is non empty set

[:(dom ([:B,B:] | x2)), the InternalRel of S:] is Relation-like set

bool [:(dom ([:B,B:] | x2)), the InternalRel of S:] is non empty set

j is Relation-like dom ([:B,B:] | x2) -defined [: the carrier of S, the carrier of S:] -valued Function-like V28( dom ([:B,B:] | x2)) quasi_total Element of bool [:(dom ([:B,B:] | x2)),[: the carrier of S, the carrier of S:]:]

a is Relation-like dom ([:B,B:] | x2) -defined the InternalRel of S -valued Function-like quasi_total Element of bool [:(dom ([:B,B:] | x2)), the InternalRel of S:]

rng a is set

b is set

x1 is set

x2 is set

[x1,x2] is non empty set

{x1,x2} is finite set

{x1} is non empty trivial finite 1 -element set

{{x1,x2},{x1}} is finite V39() set

X1 is set

B . X1 is set

X2 is set

B . X2 is set

x19 is Element of the carrier of S

x29 is Element of the carrier of S

X19 is Element of the carrier of n

X29 is Element of the carrier of n

[X1,X2] is non empty set

{X1,X2} is finite set

{X1} is non empty trivial finite 1 -element set

{{X1,X2},{X1}} is finite V39() set

[:B,B:] . (X1,X2) is set

[:B,B:] . [X1,X2] is set

a . [X1,X2] is set

n is RelStr

the carrier of n is set

[: the carrier of n, the carrier of n:] is Relation-like set

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

bool [: the carrier of n, the carrier of n:] is non empty set

the InternalRel of n ` is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

[: the carrier of n, the carrier of n:] \ the InternalRel of n is Relation-like set

id the carrier of n is Relation-like the carrier of n -defined the carrier of n -valued Function-like one-to-one V28( the carrier of n) quasi_total Element of bool [: the carrier of n, the carrier of n:]

( the InternalRel of n `) \ (id the carrier of n) is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

S is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

RelStr(# the carrier of n,S #) is strict RelStr

the carrier of RelStr(# the carrier of n,S #) is set

the InternalRel of RelStr(# the carrier of n,S #) is Relation-like the carrier of RelStr(# the carrier of n,S #) -defined the carrier of RelStr(# the carrier of n,S #) -valued Element of bool [: the carrier of RelStr(# the carrier of n,S #), the carrier of RelStr(# the carrier of n,S #):]

[: the carrier of RelStr(# the carrier of n,S #), the carrier of RelStr(# the carrier of n,S #):] is Relation-like set

bool [: the carrier of RelStr(# the carrier of n,S #), the carrier of RelStr(# the carrier of n,S #):] is non empty set

S is strict RelStr

the carrier of S is set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

[: the carrier of S, the carrier of S:] is Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

T is strict RelStr

the carrier of T is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is Relation-like set

bool [: the carrier of T, the carrier of T:] is non empty set

n is non empty RelStr

(n) is strict RelStr

the carrier of (n) is set

the carrier of n is non empty set

n is RelStr

S is RelStr

the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]

the carrier of n is set

[: the carrier of n, the carrier of n:] is Relation-like set

bool [: the carrier of n, the carrier of n:] is non empty set

card the InternalRel of n is epsilon-transitive epsilon-connected ordinal cardinal set

the InternalRel of S is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

the carrier of S is set

[: the carrier of S, the carrier of S:] is Relation-like set

bool [: the carrier of S, the carrier of S:] is non empty set

card the InternalRel of S is epsilon-transitive epsilon-connected ordinal cardinal set

[: the carrier of n, the carrier of S:] is Relation-like set

bool [: the carrier of n, the carrier of S:] is non empty set

T is empty trivial finite {} -element RelStr

the InternalRel of T is Relation-like non-empty empty-yielding the carrier of T -defined the carrier of T -valued Function-like one-to-one constant functional empty trivial non proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V23() V24() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element Function-yielding V102() Element of bool [: the carrier of T, the carrier of T:]

the carrier of T is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V23() V24() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element Function-yielding V102() set

[: the carrier of T, the carrier of T:] is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V23() V24() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element Function-yielding V102() set

bool [: the carrier of T, the carrier of T:] is non empty finite V39() set

x is empty trivial finite {} -element RelStr

the InternalRel of x is Relation-like non-empty empty-yielding the carrier of x -defined the carrier of x -valued Function-like one-to-one constant functional empty trivial non proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V23() V24() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element Function-yielding V102() Element of bool [: the carrier of x, the carrier of x:]

the carrier of x is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V23() V24() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element Function-yielding V102() set

[: the carrier of x, the carrier of x:] is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V23() V24() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element Function-yielding V102() set

bool [: the carrier of x, the carrier of x:] is non empty finite V39() set

T is Relation-like the carrier of n -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier of n, the carrier of S:]

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict RelStr

((n)) is strict () RelStr

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict RelStr

(n) is strict RelStr

((n)) is strict () RelStr

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict () RelStr

(n) is strict RelStr

((n)) is strict () RelStr

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued symmetric Element of bool [: the carrier of (n), the carrier of (n):]

the carrier of (n) is set

[: the carrier of (n), the carrier of (n):] is Relation-like set

bool [: the carrier of (n), the carrier of (n):] is non empty set

{ [b

{ [(b

{ [b

T is set

x is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

x + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[x,(x + 1)] is non empty set

{x,(x + 1)} is finite V39() set

{x} is non empty trivial finite V39() 1 -element set

{{x,(x + 1)},{x}} is finite V39() set

{ [H

T is Relation-like set

{ [H

T ~ is Relation-like set

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued Element of bool [: the carrier of (n), the carrier of (n):]

the carrier of (n) is set

[: the carrier of (n), the carrier of (n):] is Relation-like set

bool [: the carrier of (n), the carrier of (n):] is non empty set

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict () RelStr

(n) is strict RelStr

((n)) is strict () RelStr

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued symmetric Element of bool [: the carrier of (n), the carrier of (n):]

the carrier of (n) is set

[: the carrier of (n), the carrier of (n):] is Relation-like set

bool [: the carrier of (n), the carrier of (n):] is non empty set

S is set

{ [b

{ [(b

{ [b

T is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

T + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[T,(T + 1)] is non empty set

{T,(T + 1)} is finite V39() set

{T} is non empty trivial finite V39() 1 -element set

{{T,(T + 1)},{T}} is finite V39() set

x is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

x + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[(x + 1),x] is non empty set

{(x + 1),x} is finite V39() set

{(x + 1)} is non empty trivial finite V39() 1 -element set

{{(x + 1),x},{(x + 1)}} is finite V39() set

T is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

T + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[T,(T + 1)] is non empty set

{T,(T + 1)} is finite V39() set

{T} is non empty trivial finite V39() 1 -element set

{{T,(T + 1)},{T}} is finite V39() set

[(T + 1),T] is non empty set

{(T + 1),T} is finite V39() set

{(T + 1)} is non empty trivial finite V39() 1 -element set

{{(T + 1),T},{(T + 1)}} is finite V39() set

{ [b

{ [(b

{ [b

{ [(b

{ [b

{ [(b

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict () RelStr

(n) is strict RelStr

((n)) is strict () RelStr

S is set

the carrier of (n) is set

[S,S] is non empty set

{S,S} is finite set

{S} is non empty trivial finite 1 -element set

{{S,S},{S}} is finite V39() set

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued symmetric Element of bool [: the carrier of (n), the carrier of (n):]

[: the carrier of (n), the carrier of (n):] is Relation-like set

bool [: the carrier of (n), the carrier of (n):] is non empty set

{ [b

{ [(b

{ [b

x is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

x + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[x,(x + 1)] is non empty set

{x,(x + 1)} is finite V39() set

{x} is non empty trivial finite V39() 1 -element set

{{x,(x + 1)},{x}} is finite V39() set

x is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

x + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[(x + 1),x] is non empty set

{(x + 1),x} is finite V39() set

{(x + 1)} is non empty trivial finite V39() 1 -element set

{{(x + 1),x},{(x + 1)}} is finite V39() set

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict () () RelStr

(n) is strict RelStr

((n)) is strict () RelStr

the carrier of (n) is set

the carrier of (n) is set

n is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict () () RelStr

(n) is strict RelStr

((n)) is strict () RelStr

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict () () RelStr

(n) is strict RelStr

((n)) is strict () RelStr

the carrier of (n) is set

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

S is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

S + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[S,(S + 1)] is non empty set

{S,(S + 1)} is finite V39() set

{S} is non empty trivial finite V39() 1 -element set

{{S,(S + 1)},{S}} is finite V39() set

(n) is strict () () RelStr

(n) is strict RelStr

((n)) is strict () RelStr

the InternalRel of (n) is Relation-like the carrier of (n) -defined the carrier of (n) -valued finite symmetric Element of bool [: the carrier of (n), the carrier of (n):]

the carrier of (n) is finite set

[: the carrier of (n), the carrier of (n):] is Relation-like finite set

bool [: the carrier of (n), the carrier of (n):] is non empty finite V39() set

T is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

T + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT

[T,(T + 1)] is non empty set

{T,(T + 1)} is finite V39() set

{T} is non empty trivial finite V39() 1 -element set

{{T,(T + 1)},{T}} is finite V39() set

{ [b

{ [(b

{ [b

n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

(n) is strict () () RelStr

(n) is strict RelStr

((n)) is strict () RelStr

the carrier of (n) is finite set

S is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set

n is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real