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

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

bool NAT is non empty non trivial non finite set

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

[:2,2:] is non empty finite set

[:[:2,2:],2:] is non empty finite set

bool [:[:2,2:],2:] is non empty finite V41() set

K385() is set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real V36() finite V41() cardinal {} -element set

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

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

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real V36() finite V41() cardinal {} -element Element of NAT

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

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

FinSETS is non empty epsilon-transitive universal subset-closed Tarski set

Tarski-Class {} is non empty epsilon-transitive universal subset-closed Tarski set

Rank omega is epsilon-transitive set

R is non empty epsilon-transitive universal subset-closed Tarski set

N4 is set

C is set

[:N4,C:] is set

bool [:N4,C:] is non empty set

k is Relation-like N4 -defined C -valued Element of bool [:N4,C:]

Necklace 4 is strict RelStr

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

the carrier of (Necklace 4) is set

[: the carrier of (Necklace 4), the carrier of (Necklace 4):] is set

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

[0,1] is set

{0,1} is non empty finite V41() set

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

{{0,1},{0}} is non empty finite V41() set

[1,0] is set

{1,0} is non empty finite V41() set

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

{{1,0},{1}} is non empty finite V41() set

[1,2] is set

{1,2} is non empty finite V41() set

{{1,2},{1}} is non empty finite V41() set

[2,1] is set

{2,1} is non empty finite V41() set

{2} is non empty trivial finite V41() 1 -element set

{{2,1},{2}} is non empty finite V41() set

[2,3] is set

{2,3} is non empty finite V41() set

{{2,3},{2}} is non empty finite V41() set

[3,2] is set

{3,2} is non empty finite V41() set

{3} is non empty trivial finite V41() 1 -element set

{{3,2},{3}} is non empty finite V41() set

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

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

[(0 + 1),0] is set

{(0 + 1),0} is non empty finite V41() set

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

{{(0 + 1),0},{(0 + 1)}} is non empty finite V41() set

{ [(b

{ [b

{ [b

C is set

k is set

m is set

[k,m] is set

{k,m} is non empty finite set

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

{{k,m},{k}} is non empty finite V41() set

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

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

[S,(S + 1)] is set

{S,(S + 1)} is non empty finite V41() set

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

{{S,(S + 1)},{S}} is non empty finite V41() set

1 + 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

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

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

[(S + 1),S] is set

{(S + 1),S} is non empty finite V41() set

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

{{(S + 1),S},{(S + 1)}} is non empty finite V41() set

1 + 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

2 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

[(2 + 1),(1 + 1)] is set

{(2 + 1),(1 + 1)} is non empty finite V41() set

{(2 + 1)} is non empty trivial finite V41() 1 -element set

{{(2 + 1),(1 + 1)},{(2 + 1)}} is non empty finite V41() set

[(1 + 1),(2 + 1)] is set

{(1 + 1),(2 + 1)} is non empty finite V41() set

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

{{(1 + 1),(2 + 1)},{(1 + 1)}} is non empty finite V41() set

[(1 + 1),(0 + 1)] is set

{(1 + 1),(0 + 1)} is non empty finite V41() set

{{(1 + 1),(0 + 1)},{(1 + 1)}} is non empty finite V41() set

[(0 + 1),(1 + 1)] is set

{(0 + 1),(1 + 1)} is non empty finite V41() set

{{(0 + 1),(1 + 1)},{(0 + 1)}} is non empty finite V41() set

[0,(0 + 1)] is set

{0,(0 + 1)} is non empty finite V41() set

{{0,(0 + 1)},{0}} is non empty finite V41() set

C is set

R is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

Rank R is epsilon-transitive set

C is Element of Rank R

N4 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

Rank N4 is epsilon-transitive set

R is set

N4 is epsilon-transitive epsilon-connected ordinal set

Rank N4 is epsilon-transitive set

C is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

Rank C is epsilon-transitive set

R is Element of FinSETS

[:{0,1},{0,1}:] is non empty finite set

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

id {0,1} is non empty Relation-like set

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

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

k is non empty strict RelStr

the carrier of k is non empty set

[: the carrier of (Necklace 4), the carrier of k:] is set

bool [: the carrier of (Necklace 4), the carrier of k:] is non empty set

m is Relation-like the carrier of (Necklace 4) -defined the carrier of k -valued Function-like V29( the carrier of (Necklace 4), the carrier of k) Element of bool [: the carrier of (Necklace 4), the carrier of k:]

dom m is set

m . 3 is set

m . 2 is set

m . 1 is set

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

[: the carrier of k, the carrier of k:] is non empty set

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

R is RelStr

the carrier of R is set

N4 is RelStr

the carrier of N4 is set

the carrier of R \/ the carrier of N4 is set

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

[: the carrier of R, the carrier of R:] is set

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

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

[: the carrier of N4, the carrier of N4:] is set

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

the InternalRel of R \/ the InternalRel of N4 is set

[:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):] is set

bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):] is non empty set

k is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

m is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

k \/ m is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

H1 is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

RelStr(# ( the carrier of R \/ the carrier of N4),H1 #) is strict RelStr

the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #) is set

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

[: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #):] is set

bool [: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),H1 #):] is non empty set

C is strict RelStr

the carrier of C is set

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

[: the carrier of C, the carrier of C:] is set

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

k is strict RelStr

the carrier of k is set

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

[: the carrier of k, the carrier of k:] is set

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

R is RelStr

the carrier of R is set

N4 is RelStr

the carrier of N4 is set

the carrier of R \/ the carrier of N4 is set

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

[: the carrier of R, the carrier of R:] is set

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

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

[: the carrier of N4, the carrier of N4:] is set

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

the InternalRel of R \/ the InternalRel of N4 is set

[: the carrier of R, the carrier of N4:] is set

( the InternalRel of R \/ the InternalRel of N4) \/ [: the carrier of R, the carrier of N4:] is set

[: the carrier of N4, the carrier of R:] is set

(( the InternalRel of R \/ the InternalRel of N4) \/ [: the carrier of R, the carrier of N4:]) \/ [: the carrier of N4, the carrier of R:] is set

[:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):] is set

bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):] is non empty set

S is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

H1 is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

S \/ H1 is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

k is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

(S \/ H1) \/ k is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

m is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

((S \/ H1) \/ k) \/ m is Relation-like the carrier of R \/ the carrier of N4 -defined the carrier of R \/ the carrier of N4 -valued Element of bool [:( the carrier of R \/ the carrier of N4),( the carrier of R \/ the carrier of N4):]

RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) is strict RelStr

the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) is set

the InternalRel of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) is Relation-like the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) -defined the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #) -valued Element of bool [: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #):]

[: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #):] is set

bool [: the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #), the carrier of RelStr(# ( the carrier of R \/ the carrier of N4),(((S \/ H1) \/ k) \/ m) #):] is non empty set

C is strict RelStr

the carrier of C is set

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

[: the carrier of C, the carrier of C:] is set

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

k is strict RelStr

the carrier of k is set

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

[: the carrier of k, the carrier of k:] is set

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

R is set

N4 is set

C is set

k is strict RelStr

the carrier of k is set

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

[: the carrier of k, the carrier of k:] is set

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

[ the carrier of k, the InternalRel of k] is set

{ the carrier of k, the InternalRel of k} is non empty finite set

{ the carrier of k} is non empty trivial finite 1 -element set

{{ the carrier of k, the InternalRel of k},{ the carrier of k}} is non empty finite V41() set

m is strict RelStr

the carrier of m is set

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

[: the carrier of m, the carrier of m:] is set

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

[ the carrier of m, the InternalRel of m] is set

{ the carrier of m, the InternalRel of m} is non empty finite set

{ the carrier of m} is non empty trivial finite 1 -element set

{{ the carrier of m, the InternalRel of m},{ the carrier of m}} is non empty finite V41() set

R is set

N4 is set

C is set

k is strict RelStr

the carrier of k is set

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

[: the carrier of k, the carrier of k:] is set

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

[ the carrier of k, the InternalRel of k] is set

{ the carrier of k, the InternalRel of k} is non empty finite set

{ the carrier of k} is non empty trivial finite 1 -element set

{{ the carrier of k, the InternalRel of k},{ the carrier of k}} is non empty finite V41() set

k is strict RelStr

the carrier of k is set

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

[: the carrier of k, the carrier of k:] is set

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

[ the carrier of k, the InternalRel of k] is set

{ the carrier of k, the InternalRel of k} is non empty finite set

{ the carrier of k} is non empty trivial finite 1 -element set

{{ the carrier of k, the InternalRel of k},{ the carrier of k}} is non empty finite V41() set

C is strict RelStr

the carrier of C is set

k is strict RelStr

the carrier of k is set

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

[: the carrier of k, the carrier of k:] is set

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

[ the carrier of k, the InternalRel of k] is set

{ the carrier of k, the InternalRel of k} is non empty finite set

{ the carrier of k} is non empty trivial finite 1 -element set

{{ the carrier of k, the InternalRel of k},{ the carrier of k}} is non empty finite V41() set

N4 is set

C is set

k is strict RelStr

the carrier of k is set

() is set

{} ({},{}) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real Relation-like {} -defined {} -valued V36() finite finite-yielding V41() cardinal {} -element Element of bool [:{},{}:]

[:{},{}:] is finite set

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

RelStr(# {},({} ({},{})) #) is strict RelStr

the carrier of RelStr(# {},({} ({},{})) #) is set

bool () is non empty set

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

bool (bool ()) is non empty set

R is set

N4 is set

N4 is Element of bool (bool ())

Intersect N4 is Element of bool ()

C is Element of bool ()

m is strict RelStr

the carrier of m is set

S is strict RelStr

the carrier of S is set

(m,S) is strict RelStr

(m,S) is strict RelStr

H1 is strict RelStr

the carrier of H1 is set

f is strict RelStr

the carrier of f is set

(f,H1) is strict RelStr

the carrier of m \/ the carrier of S is set

cS is strict RelStr

the carrier of cS is set

H2 is strict RelStr

the carrier of H2 is set

m is strict RelStr

the carrier of m is set

S is strict RelStr

the carrier of S is set

H1 is strict RelStr

the carrier of H1 is set

(S,H1) is strict RelStr

(S,H1) is strict RelStr

meet N4 is Element of bool ()

k is strict RelStr

the carrier of k is set

m is strict RelStr

the carrier of m is set

(k,m) is strict RelStr

(k,m) is strict RelStr

S is set

S is set

k is strict RelStr

the carrier of k is set

m is set

k is strict RelStr

the carrier of k is set

m is strict RelStr

the carrier of m is set

S is strict RelStr

the carrier of S is set

(m,S) is strict RelStr

(m,S) is strict RelStr

k is Element of bool ()

m is set

k is strict RelStr

the carrier of k is set

m is strict RelStr

the carrier of m is set

S is strict RelStr

the carrier of S is set

(m,S) is strict RelStr

(m,S) is strict RelStr

H1 is Element of bool ()

R is Element of bool ()

N4 is Element of bool ()

() is Element of bool ()

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

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

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

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

the carrier of RelStr(# {0},R #) is non empty set

R is set

C is strict RelStr

the carrier of C is set

N4 is strict RelStr

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

() \ {N4} is Element of bool ()

S is strict RelStr

the carrier of S is set

H1 is strict RelStr

the carrier of H1 is set

m is Element of bool ()

the carrier of N4 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 set

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

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

the carrier of N4 is set

[: the carrier of N4, the carrier of N4:] is set

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

the carrier of N4 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 set

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

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

[: the carrier of N4, the carrier of N4:] is set

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

H2 is non empty set

H2 \/ the carrier of H1 is non empty set

(S,H1) is strict RelStr

(S,H1) is strict RelStr

the carrier of (S,H1) is set

S is strict RelStr

the carrier of S is set

C is strict RelStr

the carrier of C is set

R is RelStr

the carrier of R is set

N4 is strict RelStr

the carrier of N4 is set

{ b

( the carrier of b

N4 is set

{ b

C is Relation-like Function-like set

dom C is set

C . 0 is set

Union C is set

k is set

m is set

C . m is set

H1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

C . H1 is set

H1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . (H1 + 1) is set

{ b

( the carrier of b

H2 is set

cS is Element of ()

cH1 is strict RelStr

the carrier of cH1 is set

cH2 is strict RelStr

the carrier of cH2 is set

(cH1,cH2) is strict RelStr

(cH1,cH2) is strict RelStr

(C . H1) \/ { b

( the carrier of b

H1 is set

H2 is Element of ()

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

C . S is set

m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

C . m is set

m + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . (m + 1) is set

{ b

( the carrier of b

(C . m) \/ { b

( the carrier of b

S is set

m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

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

C . m is set

C . S is set

H1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

m + H1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . (m + H1) is set

H1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

m + (H1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . (m + (H1 + 1)) is set

(m + H1) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . ((m + H1) + 1) is set

m + 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . (m + 0) is set

H1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

m + H1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

k is Element of bool ()

m is strict RelStr

the carrier of m is set

S is strict RelStr

the carrier of S is set

(m,S) is strict RelStr

(m,S) is strict RelStr

H1 is set

C . H1 is set

H2 is set

C . H2 is set

f is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

cS is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

max (f,cS) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . (max (f,cS)) is set

{ b

( the carrier of b

(max (f,cS)) + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . ((max (f,cS)) + 1) is set

(C . (max (f,cS))) \/ { b

( the carrier of b

C . f is set

C . cS is set

m is set

m is strict RelStr

the carrier of m is set

m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

C . m is set

m + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . (m + 1) is set

{ b

( the carrier of b

H1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

H1 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT

C . (H1 + 1) is set

C . H1 is set

(C . H1) \/ { b

( the carrier of b

H2 is strict RelStr

the carrier of H2 is set

f is strict RelStr

the carrier of f is set

(H2,f) is strict RelStr

(H2,f) is strict RelStr

H2 is Element of ()

f is strict RelStr

the carrier of f is set

cS is strict RelStr

the carrier of cS is set

(f,cS) is strict RelStr

(f,cS) is strict RelStr

H2 is strict RelStr

the carrier of H2 is set

f is strict RelStr

the carrier of f is set

(H2,f) is strict RelStr

(H2,f) is strict RelStr

m is Element of ()

S is non empty trivial finite 1 -element strict RelStr

m is set

C . m is set

m is strict RelStr

the carrier of m is set

S is strict RelStr

the carrier of S is set

(m,S) is strict RelStr

(m,S) is strict RelStr

R is non empty strict RelStr

the carrier of R is non empty set

k is strict RelStr

the carrier of k is set

C is finite Element of FinSETS

card C is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of omega

m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

S is non empty strict RelStr

the carrier of S is non empty set

card the carrier of S is non empty epsilon-transitive epsilon-connected ordinal cardinal set

S is non empty strict RelStr

the carrier of S is non empty set

card the carrier of S is non empty 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, the carrier of S:] is non empty set

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

dom the InternalRel of S is set

rng the InternalRel of S is set

[: the carrier of (Necklace 4), the carrier of S:] is set

bool [: the carrier of (Necklace 4), the carrier of S:] is non empty set

H1 is Relation-like the carrier of (Necklace 4) -defined the carrier of S -valued Function-like V29( the carrier of (Necklace 4), the carrier of S) Element of bool [: the carrier of (Necklace 4), the carrier of S:]

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

H1 . 0 is set

H1 . 1 is set

[(H1 . 0),(H1 . 1)] is set

{(H1 . 0),(H1 . 1)} is non empty finite set

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

{{(H1 . 0),(H1 . 1)},{(H1 . 0)}} is non empty finite V41() set

[0,0] is set

{0,0} is non empty finite V41() set

{{0,0},{0}} is non empty finite V41() set

H1 is strict RelStr

the carrier of H1 is set

H2 is strict RelStr

the carrier of H2 is set

(H1,H2) is strict RelStr

(H1,H2) is strict RelStr

H1 is strict RelStr

the carrier of H1 is set

H2 is strict RelStr

the carrier of H2 is set

(H1,H2) is strict RelStr

(H1,H2) is strict RelStr

[1,3] is set

{1,3} is non empty finite V41() set

{{1,3},{1}} is non empty finite V41() set

[0,2] is set

{0,2} is non empty finite V41() set

{{0,2},{0}} is non empty finite V41() set

[0,3] is set

{0,3} is non empty finite V41() set

{{0,3},{0}} is non empty finite V41() set

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

[: the carrier of H1, the carrier of H1:] is set

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

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

[: the carrier of H2, the carrier of H2:] is set

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

[: the carrier of H1, the carrier of H2:] is set

[: the carrier of H2, the carrier of H1:] 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 non empty set

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

dom the InternalRel of S is set

y is set

the InternalRel of H1 \/ the InternalRel of H2 is set

( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] is set

(( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set

rng the InternalRel of S is set

y is set

the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:] is set

( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set

the InternalRel of H1 \/ (( the InternalRel of H2 \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:]) is set

[: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] is set

the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set

the InternalRel of H1 \/ ( the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) is set

the InternalRel of H1 \/ the InternalRel of H2 is set

( the InternalRel of H1 \/ the InternalRel of H2) \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set

( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] is set

(( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set

rng the InternalRel of H1 is set

[: the carrier of (Necklace 4), the carrier of S:] is set

bool [: the carrier of (Necklace 4), the carrier of S:] is non empty set

y is Relation-like the carrier of (Necklace 4) -defined the carrier of S -valued Function-like V29( the carrier of (Necklace 4), the carrier of S) Element of bool [: the carrier of (Necklace 4), the carrier of S:]

y . 1 is set

y . 0 is set

[(y . 1),(y . 0)] is set

{(y . 1),(y . 0)} is non empty finite set

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

{{(y . 1),(y . 0)},{(y . 1)}} is non empty finite V41() set

y . 3 is set

y . 2 is set

[(y . 3),(y . 2)] is set

{(y . 3),(y . 2)} is non empty finite set

{(y . 3)} is non empty trivial finite 1 -element set

{{(y . 3),(y . 2)},{(y . 3)}} is non empty finite V41() set

[(y . 2),(y . 1)] is set

{(y . 2),(y . 1)} is non empty finite set

{(y . 2)} is non empty trivial finite 1 -element set

{{(y . 2),(y . 1)},{(y . 2)}} is non empty finite V41() set

rng the InternalRel of H2 is set

[(y . 2),(y . 3)] is set

{(y . 2),(y . 3)} is non empty finite set

{{(y . 2),(y . 3)},{(y . 2)}} is non empty finite V41() set

the carrier of H1 \/ the carrier of H2 is set

[(y . 0),(y . 1)] is set

{(y . 0),(y . 1)} is non empty finite set

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

{{(y . 0),(y . 1)},{(y . 0)}} is non empty finite V41() set

dom the InternalRel of H1 is set

[(y . 1),(y . 2)] is set

{(y . 1),(y . 2)} is non empty finite set

{{(y . 1),(y . 2)},{(y . 1)}} is non empty finite V41() set

dom the InternalRel of H2 is set

[(y . 0),(y . 2)] is set

{(y . 0),(y . 2)} is non empty finite set

{{(y . 0),(y . 2)},{(y . 0)}} is non empty finite V41() set

[(y . 0),(y . 3)] is set

{(y . 0),(y . 3)} is non empty finite set

{{(y . 0),(y . 3)},{(y . 0)}} is non empty finite V41() set

[(y . 1),(y . 3)] is set

{(y . 1),(y . 3)} is non empty finite set

{{(y . 1),(y . 3)},{(y . 1)}} is non empty finite V41() set

dom y is set

rng y is set

cH1 is set

cH2 is set

y . cH2 is set

[: the carrier of (Necklace 4), the carrier of H1:] is set

bool [: the carrier of (Necklace 4), the carrier of H1:] is non empty set

the InternalRel of H1 \/ the InternalRel of H2 is set

( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] is set

(( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set

cH1 is finite set

cH2 is finite set

cH1 \/ cH2 is finite set

cS is finite set

x is set

cH1 /\ cH2 is finite set

card cS is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of omega

card cH1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of omega

x is Element of the carrier of (Necklace 4)

y is Element of the carrier of (Necklace 4)

[x,y] is set

{x,y} is non empty finite set

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

{{x,y},{x}} is non empty finite V41() set

y . x is set

y . y is set

[(y . x),(y . y)] is set

{(y . x),(y . y)} is non empty finite set

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

{{(y . x),(y . y)},{(y . x)}} is non empty finite V41() set

[: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] is set

( the InternalRel of H1 \/ the InternalRel of H2) \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set

the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set

the InternalRel of H1 \/ ( the InternalRel of H2 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) is set

[(y . 0),(y . 3)] is set

{(y . 0),(y . 3)} is non empty finite set

{{(y . 0),(y . 3)},{(y . 0)}} is non empty finite V41() set

[(y . 1),(y . 3)] is set

{(y . 1),(y . 3)} is non empty finite set

{{(y . 1),(y . 3)},{(y . 1)}} is non empty finite V41() set

the InternalRel of H1 \/ the InternalRel of H2 is set

( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] is set

(( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:]) \/ [: the carrier of H2, the carrier of H1:] is set

[(y . 0),(y . 2)] is set

{(y . 0),(y . 2)} is non empty finite set

{{(y . 0),(y . 2)},{(y . 0)}} is non empty finite V41() set

dom y is set

rng y is set

cH1 is set

cH2 is set

y . cH2 is set

[: the carrier of (Necklace 4), the carrier of H2:] is set

bool [: the carrier of (Necklace 4), the carrier of H2:] is non empty set

cH1 is finite set

cH2 is finite set

cH1 \/ cH2 is finite set

cS is finite set

x is set

cH1 /\ cH2 is finite set

card cS is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of omega

card cH2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of omega

x is Element of the carrier of (Necklace 4)

y is Element of the carrier of (Necklace 4)

[x,y] is set

{x,y} is non empty finite set

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

{{x,y},{x}} is non empty finite V41() set

y . x is set

y . y is set

[(y . x),(y . y)] is set

{(y . x),(y . y)} is non empty finite set

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

{{(y . x),(y . y)},{(y . x)}} is non empty finite V41() set

[: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:] is set

( the InternalRel of H1 \/ the InternalRel of H2) \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set

the InternalRel of H1 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:]) is set

the InternalRel of H2 \/ ( the InternalRel of H1 \/ ([: the carrier of H1, the carrier of H2:] \/ [: the carrier of H2, the carrier of H1:])) is set

f is Relation-like the carrier of (Necklace 4) -defined the carrier of S -valued Function-like V29( the carrier of (Necklace 4), the carrier of S) Element of bool [: the carrier of (Necklace 4), the carrier of S:]

f . 0 is set

f . 1 is set

[(f . 0),(f . 1)] is set

{(f . 0),(f . 1)} is non empty finite set

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

{{(f . 0),(f . 1)},{(f . 0)}} is non empty finite V41() set

f . 3 is set

f . 2 is set

[(f . 3),(f . 2)] is set

{(f . 3),(f . 2)} is non empty finite set

{(f . 3)} is non empty trivial finite 1 -element set

{{(f . 3),(f . 2)},{(f . 3)}} is non empty finite V41() set

[(f . 2),(f . 3)] is set

{(f . 2),(f . 3)} is non empty finite set

{(f . 2)} is non empty trivial finite 1 -element set

{{(f . 2),(f . 3)},{(f . 2)}} is non empty finite V41() set

[(f . 2),(f . 1)] is set

{(f . 2),(f . 1)} is non empty finite set

{{(f . 2),(f . 1)},{(f . 2)}} is non empty finite V41() set

[(f . 1),(f . 2)] is set

{(f . 1),(f . 2)} is non empty finite set

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

{{(f . 1),(f . 2)},{(f . 1)}} is non empty finite V41() set

[(f . 1),(f . 0)] is set

{(f . 1),(f . 0)} is non empty finite set

{{(f . 1),(f . 0)},{(f . 1)}} is non empty finite V41() set

dom f is set

cH1 is finite set

cH2 is finite set

cH1 \/ cH2 is finite set

the InternalRel of H1 \/ the InternalRel of H2 is set

cS is finite set

y is set

cH1 /\ cH2 is finite set

card cS is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of omega

card cH1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of omega

y is Element of the carrier of (Necklace 4)

x is Element of the carrier of (Necklace 4)

[y,x] is set

{y,x} is non empty finite set

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

{{y,x},{y}} is non empty finite V41() set

f . y is set

f . x is set

[(f . y),(f . x)] is set

{(f . y),(f . x)} is non empty finite set

{(f . y)} is non empty trivial finite 1 -element set

{{(f . y),(f . x)},{(f . y)}} is non empty finite V41() set

rng f is set

y is set

x is set

f . x is set

[: the carrier of (Necklace 4), the carrier of H1:] is set

bool [: the carrier of (Necklace 4), the carrier of H1:] is non empty set

dom f is set

cH1 is finite set

cH2 is finite set

cH1 \/ cH2 is finite set

the InternalRel of H1 \/ the InternalRel of H2 is set

cS is finite set

y is set

cH1 /\ cH2 is finite set

card cS is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of omega

card cH2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of omega

y is Element of the carrier of (Necklace 4)

x is Element of the carrier of (Necklace 4)

[y,x] is set

{y,x} is non empty finite set

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

{{y,x},{y}} is non empty finite V41() set

f . y is set

f . x is set

[(f . y),(f . x)] is set

{(f . y),(f . x)} is non empty finite set

{(f . y)} is non empty trivial finite 1 -element set

{{(f . y),(f . x)},{(f . y)}} is non empty finite V41() set

rng f is set

y is set

x is set

f . x is set

[: the carrier of (Necklace 4), the carrier of H2:] is set

bool [: the carrier of (Necklace 4), the carrier of H2:] is non empty set

f is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

cS is non empty strict RelStr

the carrier of cS is non empty set

card the carrier of cS is non empty epsilon-transitive epsilon-connected ordinal cardinal set

cH1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal set

cH2 is non empty strict RelStr

the carrier of cH2 is non empty set

card the carrier of cH2 is non empty epsilon-transitive epsilon-connected ordinal cardinal set

m is non empty strict RelStr

the carrier of m is non empty set

card the carrier of m is non empty epsilon-transitive epsilon-connected ordinal cardinal set

m is non empty strict RelStr

the carrier of m is non empty set

card the carrier of m is non empty epsilon-transitive epsilon-connected ordinal cardinal set