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
{ [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT : not 4 <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT : not 4 <= b1 + 1 } is set
{ [b1,(b1 + 1)] where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT : not 4 <= b1 + 1 } \/ { [(b1 + 1),b1] where b1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V36() finite cardinal Element of NAT : not 4 <= b1 + 1 } is set
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
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in a2 & b3 in a2 & ( b1 = (b2,b3) or b1 = (b2,b3) ) ) } is set
N4 is set
{ b1 where b1 is Element of () : b1 is trivial finite RelStr } is set
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
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . H1 & b3 in C . H1 & ( b1 = (b2,b3) or b1 = (b2,b3) ) ) } is set
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) \/ { b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . H1 & b3 in C . H1 & ( b1 = (b2,b3) or b1 = (b2,b3) ) ) } is set
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
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . m & b3 in C . m & ( b1 = (b2,b3) or b1 = (b2,b3) ) ) } is set
(C . m) \/ { b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . m & b3 in C . m & ( b1 = (b2,b3) or b1 = (b2,b3) ) ) } is set
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
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . (max (f,cS)) & b3 in C . (max (f,cS)) & ( b1 = (b2,b3) or b1 = (b2,b3) ) ) } is set
(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))) \/ { b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . (max (f,cS)) & b3 in C . (max (f,cS)) & ( b1 = (b2,b3) or b1 = (b2,b3) ) ) } is set
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
{ b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . m & b3 in C . m & ( b1 = (b2,b3) or b1 = (b2,b3) ) ) } is set
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) \/ { b1 where b1 is Element of () : ex b2, b3 being strict RelStr st
( the carrier of b2 misses the carrier of b3 & b2 in C . m & b3 in C . m & ( b1 = (b2,b3) or b1 = (b2,b3) ) ) } is set
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