:: NECKLACE semantic presentation

REAL is set

bool REAL is non empty set

bool omega is non empty non trivial non finite set
{} is set

{{},1} is finite set
bool NAT is non empty non trivial non finite set

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},{i,x1}:] is Relation-like finite set
[:{n},{x}:] \/ [:{n},{i,x1}:] 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]} \/ [:{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

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not T <= b1 } is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not S <= b1 } is set
n is set

[: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 () is set
x is set
() . T is set
() . x is set
dom () 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

[:n,n:] is Relation-like set
bool [:n,n:] is non empty set

Funcs (n,n) is functional non empty set

S is set
dom n is set
T is set
n . S is set
n . T is set

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

dom n is set

dom S is set

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

dom n is 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
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) . 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

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

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

{T} is non empty trivial finite 1 -element 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} is non empty trivial finite 1 -element set

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

bool [:{n},{S}:] is non empty finite V39() 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} is non empty trivial finite 1 -element set

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

bool [:{n},{x}:] is non empty finite V39() 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
F2() is Relation-like set
F1() is non empty set
{ [F4(b1),F3(b1)] where b1 is Element of F1() : P1[b1] } is set
F2() ~ is Relation-like set
{ [F3(b1),F4(b1)] where b1 is Element of F1() : P1[b1] } is set
S is set
T is Element of F1()
F3(T) is set
F4(T) is set
[F3(T),F4(T)] is non empty set
{F3(T),F4(T)} is finite set
{F3(T)} is non empty trivial finite 1 -element set
{{F3(T),F4(T)},{F3(T)}} is finite V39() 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 F1()
F4(i) is set
F3(i) is set
[F4(i),F3(i)] is non empty set
{F4(i),F3(i)} is finite set
{F4(i)} is non empty trivial finite 1 -element set
{{F4(i),F3(i)},{F4(i)}} is finite V39() 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
i is Element of F1()
F3(i) is set
F4(i) is set
[F3(i),F4(i)] is non empty set
{F3(i),F4(i)} is finite set
{F3(i)} is non empty trivial finite 1 -element set
{{F3(i),F4(i)},{F3(i)}} is finite V39() 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

{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set

T is set

[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

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 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
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set

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

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

{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S1[b1] } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S2[b1] } is set

[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,(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
{ H2(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : b1 in n -' 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
card { [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is epsilon-transitive epsilon-connected ordinal cardinal 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 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
is non empty trivial finite V39() 1 -element set
is finite V39() set

bool is non empty finite V39() set

RelStr(# ,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

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

[: 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:]

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

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

[: 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

bool [: the carrier of T, the carrier of T:] is non empty finite V39() 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 strict RelStr
((n)) is strict () RelStr

(n) is strict RelStr
(n) is strict RelStr
((n)) is strict () RelStr

(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
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } \/ { [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
T is set

[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
{ [H2(b1),H1(b1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S1[b1] } is set

{ [H1(b1),H2(b1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S1[b1] } is 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 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
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } \/ { [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set

[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 + 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,(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
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } \/ { [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } \/ { [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is 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
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } \/ { [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set

[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 + 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 strict () () RelStr
(n) is strict RelStr
((n)) is strict () RelStr
the carrier of (n) is set
the carrier of (n) is set

(n) is strict () () RelStr
(n) is strict RelStr
((n)) is strict () RelStr

(n) is strict () () RelStr
(n) is strict RelStr
((n)) is strict () RelStr
the carrier of (n) is set

[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,(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
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } \/ { [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b1 + 1 } is set

(n) is strict () () RelStr
(n) is strict RelStr
((n)) is strict () RelStr
the carrier of (n) is finite set