:: 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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not T <= b₁ } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not S <= b₁ } is set
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₂() is Relation-like set
F₁() is non empty set
{ [F₄(b₁),F₃(b₁)] where b₁ is Element of F₁() : P₁[b₁] } is set
F₂() ~ is Relation-like set
{ [F₃(b₁),F₄(b₁)] where b₁ is Element of F₁() : P₁[b₁] } is set
S is set
T is Element of F₁()
F₃(T) is set
F₄(T) is set
[F₃(T),F₄(T)] is non empty set
{F₃(T),F₄(T)} is finite set
{F₃(T)} is non empty trivial finite 1 -element set
{{F₃(T),F₄(T)},{F₃(T)}} is finite V39() set
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₄(i) is set
F₃(i) is set
[F₄(i),F₃(i)] is non empty set
{F₄(i),F₃(i)} is finite set
{F₄(i)} is non empty trivial finite 1 -element set
{{F₄(i),F₃(i)},{F₄(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 F₁()
F₃(i) is set
F₄(i) is set
[F₃(i),F₄(i)] is non empty set
{F₃(i),F₄(i)} is finite set
{F₃(i)} is non empty trivial finite 1 -element set
{{F₃(i),F₄(i)},{F₃(i)}} is finite V39() set
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₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
[: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₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
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₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₁[b₁] } is set
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₂[b₁] } is set
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₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : b₁ in n -' 1 } is set
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
card { [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is epsilon-transitive epsilon-connected ordinal cardinal set
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₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } \/ { [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is 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
{ [H₂(b₁),H₁(b₁)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₁[b₁] } is set
T is Relation-like set
{ [H₁(b₁),H₂(b₁)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₁[b₁] } is set
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₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } \/ { [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is 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
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₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } \/ { [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } \/ { [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is 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
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₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } \/ { [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } 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
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₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } \/ { [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is 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 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 finite cardinal set
(n) is non empty strict () () RelStr
(n) is strict RelStr
((n)) is strict () RelStr
the carrier of (n) is non empty finite set
bool the carrier of (n) is non empty finite V39() set
[#] (n) is non empty non proper finite Element of bool the carrier of (n)
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), the carrier of (n):] is Relation-like non empty finite set
bool [: the carrier of (n), the carrier of (n):] is non empty finite V39() set
S is finite Element of bool the carrier of (n)
T is finite Element of bool the carrier of (n)
S \/ T is finite Element of bool the carrier of (n)
the InternalRel of (n) |_2 S is Relation-like set
[:S,S:] is Relation-like finite set
the InternalRel of (n) /\ [:S,S:] is Relation-like the carrier of (n) -defined the carrier of (n) -valued finite set
the InternalRel of (n) |_2 T is Relation-like set
[:T,T:] is Relation-like finite set
the InternalRel of (n) /\ [:T,T:] is Relation-like the carrier of (n) -defined the carrier of (n) -valued finite set
( the InternalRel of (n) |_2 S) \/ ( the InternalRel of (n) |_2 T) is Relation-like set
x is Element of the carrier of (n)
i is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
x1 + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
x2 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
x2 + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
[x2,(x2 + 1)] is non empty set
{x2,(x2 + 1)} is finite V39() set
{x2} is non empty trivial finite V39() 1 -element set
{{x2,(x2 + 1)},{x2}} is finite V39() set
x is Element of the carrier of (n)
i is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
x1 + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
x2 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
x2 + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
[x2,(x2 + 1)] is non empty set
{x2,(x2 + 1)} is finite V39() set
{x2} is non empty trivial finite V39() 1 -element set
{{x2,(x2 + 1)},{x2}} 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 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
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 set
[S,T] is non empty set
{S,T} is finite V39() set
{S} is non empty trivial finite V39() 1 -element set
{{S,T},{S}} is finite V39() set
T + 1 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
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } \/ { [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } 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
x is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
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
x is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
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 finite set
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), the carrier of (n):] is Relation-like finite set
bool [: the carrier of (n), the carrier of (n):] is non empty finite V39() 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 set
T + 1 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,T] is non empty set
{S,T} is finite V39() set
{S} is non empty trivial finite V39() 1 -element set
{{S,T},{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
[(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
the InternalRel of (n) ~ is Relation-like the carrier of (n) -defined the carrier of (n) -valued finite Element of bool [: the carrier of (n), the carrier of (n):]
n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
card { [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } 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
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 + 1),S] is non empty set
{(S + 1),S} is finite V39() set
{(S + 1)} is non empty trivial finite V39() 1 -element set
{{(S + 1),S},{(S + 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 + 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
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₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₁[b₁] } is set
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₂[b₁] } is set
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : b₁ in n -' 1 } is set
card (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega
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 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
card the InternalRel of (n) is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega
n - 1 is V23() V24() ext-real Element of REAL
2 * (n - 1) is V23() V24() ext-real Element of REAL
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is set
{ [H₁(b₁),H₂(b₁)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₁[b₁] } is set
x is set
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
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } \/ { [H₁(b₁),H₂(b₁)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₁[b₁] } is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real non negative finite cardinal Element of NAT
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 { [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not n <= b₁ + 1 } is epsilon-transitive epsilon-connected ordinal cardinal set
x is Relation-like set
{ [H₂(b₁),H₁(b₁)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₁[b₁] } is set
x ~ is Relation-like set
i 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
[x2,x1] is non empty set
{x2,x1} is finite set
{x2} is non empty trivial finite 1 -element set
{{x2,x1},{x2}} is finite V39() set
B is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
B + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
[B,(B + 1)] is non empty set
{B,(B + 1)} is finite V39() set
{B} is non empty trivial finite V39() 1 -element set
{{B,(B + 1)},{B}} is finite V39() set
F is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
F + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
[F,(F + 1)] is non empty set
{F,(F + 1)} is finite V39() set
{F} is non empty trivial finite V39() 1 -element set
{{F,(F + 1)},{F}} is finite V39() set
card { [H₁(b₁),H₂(b₁)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : S₁[b₁] } is epsilon-transitive epsilon-connected ordinal cardinal set
card (n - 1) is epsilon-transitive epsilon-connected ordinal cardinal set
(card (n - 1)) +` (card (n - 1)) is epsilon-transitive epsilon-connected ordinal cardinal set
(n -' 1) + (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real non negative finite cardinal Element of NAT
card ((n -' 1) + (n -' 1)) is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega
(1) is non empty strict () () RelStr
(1) is strict RelStr
((1)) is strict () RelStr
((1)) is non empty strict RelStr
0 .--> 0 is Relation-like NAT -defined {0} -defined NAT -valued Function-like one-to-one constant trivial finite set
{0} is non empty trivial finite V39() 1 -element set
{0} --> 0 is Relation-like {0} -defined NAT -valued {0} -valued Function-like constant non empty V28({0}) quasi_total finite Element of bool [:{0},{0}:]
[:{0},{0}:] is Relation-like non empty finite set
bool [:{0},{0}:] is non empty finite V39() set
the carrier of (1) is non empty finite set
the carrier of ((1)) is non empty set
[: the carrier of (1), the carrier of ((1)):] is Relation-like non empty set
bool [: the carrier of (1), the carrier of ((1)):] is non empty set
x is Relation-like the carrier of (1) -defined the carrier of ((1)) -valued Function-like non empty V28( the carrier of (1)) quasi_total finite Element of bool [: the carrier of (1), the carrier of ((1)):]
rng x is non empty finite set
dom x is non empty finite Element of bool the carrier of (1)
bool the carrier of (1) is non empty finite V39() set
i is set
x1 is set
x . i is set
x . x1 is set
[: the carrier of ((1)), the carrier of (1):] is Relation-like non empty set
bool [: the carrier of ((1)), the carrier of (1):] is non empty set
x " is Relation-like Function-like set
i is Relation-like the carrier of ((1)) -defined the carrier of (1) -valued Function-like non empty V28( the carrier of ((1))) quasi_total Element of bool [: the carrier of ((1)), the carrier of (1):]
x1 is Element of the carrier of ((1))
x2 is Element of the carrier of ((1))
i . x1 is set
i . 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
the InternalRel of ((1)) is Relation-like the carrier of ((1)) -defined the carrier of ((1)) -valued Element of bool [: the carrier of ((1)), the carrier of ((1)):]
[: the carrier of ((1)), the carrier of ((1)):] is Relation-like non empty set
bool [: the carrier of ((1)), the carrier of ((1)):] is non empty set
[: the carrier of (1), the carrier of (1):] is Relation-like non empty finite set
the InternalRel of (1) is Relation-like the carrier of (1) -defined the carrier of (1) -valued finite symmetric Element of bool [: the carrier of (1), the carrier of (1):]
bool [: the carrier of (1), the carrier of (1):] is non empty finite V39() set
the InternalRel of (1) ` is Relation-like the carrier of (1) -defined the carrier of (1) -valued finite Element of bool [: the carrier of (1), the carrier of (1):]
[: the carrier of (1), the carrier of (1):] \ the InternalRel of (1) is Relation-like finite set
id the carrier of (1) is Relation-like the carrier of (1) -defined the carrier of (1) -valued Function-like one-to-one non empty V28( the carrier of (1)) quasi_total finite Element of bool [: the carrier of (1), the carrier of (1):]
( the InternalRel of (1) `) \ (id the carrier of (1)) is Relation-like the carrier of (1) -defined the carrier of (1) -valued finite Element of bool [: the carrier of (1), the carrier of (1):]
B is Element of the carrier of (1)
F is Element of the carrier of (1)
i . x1 is Element of the carrier of (1)
i . x2 is Element of the carrier of (1)
y is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
x + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
y + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
x1 is Element of the carrier of (1)
x2 is Element of the carrier of (1)
x . x1 is set
x . 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
the InternalRel of (1) is Relation-like the carrier of (1) -defined the carrier of (1) -valued finite symmetric Element of bool [: the carrier of (1), the carrier of (1):]
[: the carrier of (1), the carrier of (1):] is Relation-like non empty finite set
bool [: the carrier of (1), the carrier of (1):] is non empty finite V39() set
x is Element of the carrier of ((1))
y is Element of the carrier of ((1))
x . x1 is Element of the carrier of ((1))
x . x2 is Element of the carrier of ((1))
B is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
F is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
F + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
B + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
(4) is non empty strict () () RelStr
(4) is strict RelStr
((4)) is strict () RelStr
((4)) is non empty strict RelStr
(0,1) --> (1,3) is Relation-like NAT -defined {0,1} -defined NAT -valued Function-like V28({0,1}) quasi_total finite Element of bool [:{0,1},NAT:]
{0,1} is finite V39() set
[:{0,1},NAT:] is Relation-like set
bool [:{0,1},NAT:] is non empty set
(2,3) --> (0,2) is Relation-like NAT -defined {2,3} -defined NAT -valued Function-like V28({2,3}) quasi_total finite Element of bool [:{2,3},NAT:]
{2,3} is finite V39() set
[:{2,3},NAT:] is Relation-like set
bool [:{2,3},NAT:] is non empty set
((0,1) --> (1,3)) +* ((2,3) --> (0,2)) is Relation-like NAT -defined NAT -valued Function-like finite set
rng ((2,3) --> (0,2)) is finite set
{0,2} is finite V39() set
rng ((0,1) --> (1,3)) is finite set
{1,3} is finite V39() set
rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) is finite set
the carrier of ((4)) is non empty set
x1 is set
(rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) is finite set
{1,3,0,2} is non empty finite set
the carrier of (4) is non empty finite set
dom (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) is finite set
dom ((0,1) --> (1,3)) is finite V39() Element of bool {0,1}
bool {0,1} is non empty finite V39() set
dom ((2,3) --> (0,2)) is finite V39() Element of bool {2,3}
bool {2,3} is non empty finite V39() set
(dom ((0,1) --> (1,3))) \/ (dom ((2,3) --> (0,2))) is finite V39() set
{0,1} \/ (dom ((2,3) --> (0,2))) is finite V39() set
{0,1} \/ {2,3} is finite V39() set
the carrier of (4) is non empty finite set
[: the carrier of (4), the carrier of ((4)):] is Relation-like non empty set
bool [: the carrier of (4), the carrier of ((4)):] is non empty set
x1 is Relation-like the carrier of (4) -defined the carrier of ((4)) -valued Function-like non empty V28( the carrier of (4)) quasi_total finite Element of bool [: the carrier of (4), the carrier of ((4)):]
[: the carrier of ((4)), the carrier of (4):] is Relation-like non empty set
bool [: the carrier of ((4)), the carrier of (4):] is non empty set
x1 " is Relation-like Function-like set
the InternalRel of ((4)) is Relation-like the carrier of ((4)) -defined the carrier of ((4)) -valued Element of bool [: the carrier of ((4)), the carrier of ((4)):]
[: the carrier of ((4)), the carrier of ((4)):] is Relation-like non empty set
bool [: the carrier of ((4)), the carrier of ((4)):] is non empty set
0 .--> 1 is Relation-like NAT -defined {0} -defined NAT -valued Function-like one-to-one constant trivial finite set
{0} is non empty trivial finite V39() 1 -element set
{0} --> 1 is Relation-like non-empty {0} -defined NAT -valued {1} -valued Function-like constant non empty V28({0}) quasi_total finite Element of bool [:{0},{1}:]
{1} is non empty trivial finite V39() 1 -element set
[:{0},{1}:] is Relation-like non empty finite set
bool [:{0},{1}:] is non empty finite V39() set
rng (0 .--> 1) is trivial finite set
1 .--> 3 is Relation-like NAT -defined {1} -defined NAT -valued Function-like one-to-one constant trivial finite set
{1} --> 3 is Relation-like non-empty {1} -defined NAT -valued {3} -valued Function-like constant non empty V28({1}) quasi_total finite Element of bool [:{1},{3}:]
{3} is non empty trivial finite V39() 1 -element set
[:{1},{3}:] is Relation-like non empty finite set
bool [:{1},{3}:] is non empty finite V39() set
rng (1 .--> 3) is trivial finite set
B is set
B is set
[1,3] is non empty set
{{1,3},{1}} is finite V39() set
[3,1] is non empty set
{3,1} is finite V39() set
{{3,1},{3}} is finite V39() set
[0,2] is non empty set
{{0,2},{0}} is finite V39() set
[2,0] is non empty set
{2,0} is finite V39() set
{2} is non empty trivial finite V39() 1 -element set
{{2,0},{2}} is finite V39() set
[0,3] is non empty set
{0,3} is finite V39() set
{{0,3},{0}} is finite V39() set
[3,0] is non empty set
{3,0} is finite V39() set
{{3,0},{3}} is finite V39() set
{[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} is non empty finite set
2 .--> 0 is Relation-like NAT -defined {2} -defined NAT -valued Function-like one-to-one constant trivial finite set
{2} --> 0 is Relation-like {2} -defined NAT -valued {0} -valued Function-like constant non empty V28({2}) quasi_total finite Element of bool [:{2},{0}:]
[:{2},{0}:] is Relation-like non empty finite set
bool [:{2},{0}:] is non empty finite V39() set
rng (2 .--> 0) is trivial finite set
3 .--> 2 is Relation-like NAT -defined {3} -defined NAT -valued Function-like one-to-one constant trivial finite set
{3} --> 2 is Relation-like non-empty {3} -defined NAT -valued {2} -valued Function-like constant non empty V28({3}) quasi_total finite Element of bool [:{3},{2}:]
[:{3},{2}:] is Relation-like non empty finite set
bool [:{3},{2}:] is non empty finite V39() set
rng (3 .--> 2) is trivial finite set
F is set
(2 .--> 0) +* (3 .--> 2) is Relation-like NAT -defined NAT -valued Function-like finite set
F is set
rng x1 is non empty finite set
(rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) is finite set
{1,3,0,2} is non empty finite set
(0 .--> 1) +* (1 .--> 3) is Relation-like NAT -defined NAT -valued Function-like finite set
y is set
[: the carrier of (4), the carrier of (4):] is Relation-like non empty finite set
i is Element of [: the carrier of (4), the carrier of (4):]
the InternalRel of (4) is Relation-like the carrier of (4) -defined the carrier of (4) -valued finite symmetric Element of bool [: the carrier of (4), the carrier of (4):]
bool [: the carrier of (4), the carrier of (4):] is non empty finite V39() set
j is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
j + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
[j,(j + 1)] is non empty set
{j,(j + 1)} is finite V39() set
{j} is non empty trivial finite V39() 1 -element set
{{j,(j + 1)},{j}} is finite V39() set
[(j + 1),j] is non empty set
{(j + 1),j} is finite V39() set
{(j + 1)} is non empty trivial finite V39() 1 -element set
{{(j + 1),j},{(j + 1)}} is finite V39() set
the InternalRel of (4) ` is Relation-like the carrier of (4) -defined the carrier of (4) -valued finite Element of bool [: the carrier of (4), the carrier of (4):]
[: the carrier of (4), the carrier of (4):] \ the InternalRel of (4) is Relation-like finite set
id the carrier of (4) is Relation-like the carrier of (4) -defined the carrier of (4) -valued Function-like one-to-one non empty V28( the carrier of (4)) quasi_total finite Element of bool [: the carrier of (4), the carrier of (4):]
( the InternalRel of (4) `) \ (id the carrier of (4)) is Relation-like the carrier of (4) -defined the carrier of (4) -valued finite Element of bool [: the carrier of (4), the carrier of (4):]
x1 . 2 is set
((2,3) --> (0,2)) . 2 is set
x1 . 3 is set
((2,3) --> (0,2)) . 3 is set
x1 . 0 is set
((0,1) --> (1,3)) . 0 is set
x1 . 1 is set
((0,1) --> (1,3)) . 1 is set
x is Element of the carrier of (4)
y is Element of the carrier of (4)
x1 . x is set
x1 . y is set
[x,y] is non empty set
{x,y} is finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is finite V39() set
the InternalRel of (4) is Relation-like the carrier of (4) -defined the carrier of (4) -valued finite symmetric Element of bool [: the carrier of (4), the carrier of (4):]
[: the carrier of (4), the carrier of (4):] is Relation-like non empty finite set
bool [: the carrier of (4), the carrier of (4):] is non empty finite V39() set
i is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
j is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal set
j + 1 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
a is Element of the carrier of ((4))
b is Element of the carrier of ((4))
x1 . x is Element of the carrier of ((4))
x1 . y is Element of the carrier of ((4))
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
F is Relation-like the carrier of ((4)) -defined the carrier of (4) -valued Function-like non empty V28( the carrier of ((4))) quasi_total Element of bool [: the carrier of ((4)), the carrier of (4):]
x is Element of the carrier of ((4))
y is Element of the carrier of ((4))
F . x is set
F . y is set
[x,y] is non empty set
{x,y} is finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is finite V39() set
[: the carrier of (4), the carrier of (4):] is Relation-like non empty finite set
the InternalRel of (4) is Relation-like the carrier of (4) -defined the carrier of (4) -valued finite symmetric Element of bool [: the carrier of (4), the carrier of (4):]
bool [: the carrier of (4), the carrier of (4):] is non empty finite V39() set
the InternalRel of (4) ` is Relation-like the carrier of (4) -defined the carrier of (4) -valued finite Element of bool [: the carrier of (4), the carrier of (4):]
[: the carrier of (4), the carrier of (4):] \ the InternalRel of (4) is Relation-like finite set
id the carrier of (4) is Relation-like the carrier of (4) -defined the carrier of (4) -valued Function-like one-to-one non empty V28( the carrier of (4)) quasi_total finite Element of bool [: the carrier of (4), the carrier of (4):]
( the InternalRel of (4) `) \ (id the carrier of (4)) is Relation-like the carrier of (4) -defined the carrier of (4) -valued finite Element of bool [: the carrier of (4), the carrier of (4):]
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not 4 <= b₁ + 1 } is set
{ [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not 4 <= b₁ + 1 } is set
{ [b₁,(b₁ + 1)] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not 4 <= b₁ + 1 } \/ { [(b₁ + 1),b₁] where b₁ is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT : not 4 <= b₁ + 1 } is set
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
j is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
j + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
((2,3) --> (0,2)) " is Relation-like Function-like set
(0,2) --> (2,3) is Relation-like NAT -defined {0,2} -defined NAT -valued Function-like V28({0,2}) quasi_total finite Element of bool [:{0,2},NAT:]
[:{0,2},NAT:] is Relation-like set
bool [:{0,2},NAT:] is non empty set
dom (((2,3) --> (0,2)) ") is set
F . 0 is set
((0,1) --> (1,3)) " is Relation-like Function-like set
(((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ") is Relation-like Function-like set
((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 0 is set
(((2,3) --> (0,2)) ") . 0 is set
(1,3) --> (0,1) is Relation-like NAT -defined {1,3} -defined NAT -valued Function-like V28({1,3}) quasi_total finite Element of bool [:{1,3},NAT:]
[:{1,3},NAT:] is Relation-like set
bool [:{1,3},NAT:] is non empty set
dom (((0,1) --> (1,3)) ") is set
a is set
F . 1 is set
((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 1 is set
(((0,1) --> (1,3)) ") . 1 is set
F . 2 is set
((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 2 is set
(((2,3) --> (0,2)) ") . 2 is set
F . 3 is set
((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 3 is set
(((0,1) --> (1,3)) ") . 3 is set
a is Element of the carrier of (4)
b is Element of the carrier of (4)
F . x is Element of the carrier of (4)
F . y is Element of the carrier of (4)
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is finite V39() set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of NAT
[a,b] is non empty set
{a,b} is finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} 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
((n)) is strict RelStr
card n is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega
[:n,n:] is Relation-like finite set
card [:n,n:] is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega
n * n is V23() V24() ext-real set
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
card the InternalRel of (n) is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega
n - 1 is V23() V24() ext-real Element of REAL
2 * (n - 1) is V23() V24() ext-real Element of REAL
(n * n) - (2 * (n - 1)) is V23() V24() ext-real Element of REAL
((n * n) - (2 * (n - 1))) - n is V23() V24() ext-real Element of REAL
5 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT
- 5 is V23() V24() ext-real non positive Element of REAL
delta (1,(- 5),4) is V23() V24() ext-real Element of REAL
(- 5) ^2 is V23() V24() ext-real Element of REAL
(- 5) * (- 5) is V23() V24() ext-real non negative set
4 * 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real non negative finite cardinal Element of NAT
(4 * 1) * 4 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real non negative finite cardinal Element of NAT
((- 5) ^2) - ((4 * 1) * 4) is V23() V24() ext-real Element of REAL
9 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT
n ^2 is V23() V24() ext-real set
1 * (n ^2) is V23() V24() ext-real Element of REAL
(- 5) * n is V23() V24() ext-real Element of REAL
(1 * (n ^2)) + ((- 5) * n) is V23() V24() ext-real Element of REAL
((1 * (n ^2)) + ((- 5) * n)) + 4 is V23() V24() ext-real Element of REAL
- (- 5) is V23() V24() ext-real non negative Element of REAL
sqrt (delta (1,(- 5),4)) is V23() V24() ext-real Element of REAL
(- (- 5)) - (sqrt (delta (1,(- 5),4))) is V23() V24() ext-real Element of REAL
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real non negative finite cardinal Element of NAT
((- (- 5)) - (sqrt (delta (1,(- 5),4)))) / (2 * 1) is V23() V24() ext-real Element of REAL
(- (- 5)) + (sqrt (delta (1,(- 5),4))) is V23() V24() ext-real Element of REAL
((- (- 5)) + (sqrt (delta (1,(- 5),4)))) / (2 * 1) is V23() V24() ext-real Element of REAL
3 ^2 is V23() V24() ext-real Element of REAL
3 * 3 is V23() V24() ext-real non negative set
sqrt (3 ^2) is V23() V24() ext-real Element of REAL
5 - (sqrt (3 ^2)) is V23() V24() ext-real Element of REAL
(5 - (sqrt (3 ^2))) / 2 is V23() V24() ext-real Element of REAL
5 + (sqrt (3 ^2)) is V23() V24() ext-real Element of REAL
(5 + (sqrt (3 ^2))) / 2 is V23() V24() ext-real Element of REAL
5 - 3 is V23() V24() ext-real Element of REAL
(5 - 3) / 2 is V23() V24() ext-real Element of REAL
5 + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real positive non negative finite cardinal Element of NAT
(5 + 3) / 2 is V23() V24() ext-real non negative Element of REAL
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 finite Element of bool [: the carrier of (n), the carrier of (n):]
x is set
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
[(i + 1),i] is non empty set
{(i + 1),i} is finite V39() set
{(i + 1)} is non empty trivial finite V39() 1 -element set
{{(i + 1),i},{(i + 1)}} is finite V39() 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
the InternalRel of (n) ` is Relation-like the carrier of (n) -defined the carrier of (n) -valued finite 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 finite set
card ( the InternalRel of (n) `) is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega
card (id the carrier of (n)) is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega
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 (n) `) \ (id the carrier of (n)) is Relation-like the carrier of (n) -defined the carrier of (n) -valued finite Element of bool [: the carrier of (n), the carrier of (n):]
card (( the InternalRel of (n) `) \ (id the carrier of (n))) is epsilon-transitive epsilon-connected ordinal natural V23() V24() ext-real finite cardinal Element of omega