REAL is set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
2 is non empty V4() V5() V6() V10() V11() ext-real positive non negative finite cardinal V71() Element of NAT
[:2,2:] is non empty Relation-like finite set
[:[:2,2:],2:] is non empty Relation-like finite set
bool [:[:2,2:],2:] is non empty finite V54() set
[:NAT,NAT:] is non empty non trivial Relation-like non finite set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
K287() is non empty V155() L16()
the carrier of K287() is non empty set
K290() is Element of bool NAT
[:K290(),K290():] is Relation-like set
[:[:K290(),K290():],K290():] is Relation-like set
bool [:[:K290(),K290():],K290():] is non empty set
{} is empty trivial V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V54() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V71() Function-yielding V175() set
the empty trivial V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V54() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V71() Function-yielding V175() set is empty trivial V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V54() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V71() Function-yielding V175() set
1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative finite cardinal V71() Element of NAT
{{},1} is non empty finite V54() set
fin_RelStr is non empty set
bool fin_RelStr is non empty set
3 is non empty V4() V5() V6() V10() V11() ext-real positive non negative finite cardinal V71() Element of NAT
4 is non empty V4() V5() V6() V10() V11() ext-real positive non negative finite cardinal V71() Element of NAT
0 is empty trivial V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V54() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V71() Function-yielding V175() Element of NAT
{0,1,2,3} is non empty finite set
Necklace 4 is non empty strict symmetric irreflexive RelStr
4 -SuccRelStr is strict RelStr
SymRelStr (4 -SuccRelStr) is strict symmetric RelStr
ComplRelStr (Necklace 4) is non empty strict RelStr
FinSETS is non empty universal set
K139({}) is set
the InternalRel of (Necklace 4) is Relation-like the carrier of (Necklace 4) -defined the carrier of (Necklace 4) -valued symmetric finite Element of bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):]
the carrier of (Necklace 4) is non empty finite set
[: the carrier of (Necklace 4), the carrier of (Necklace 4):] is non empty Relation-like finite set
bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):] is non empty finite V54() set
[0,1] is non empty set
{0,1} is non empty finite V54() set
{0} is non empty trivial functional finite V54() 1 -element set
{{0,1},{0}} is non empty finite V54() set
[1,0] is non empty set
{1,0} is non empty finite V54() set
{1} is non empty trivial finite V54() 1 -element set
{{1,0},{1}} is non empty finite V54() set
[1,2] is non empty set
{1,2} is non empty finite V54() set
{{1,2},{1}} is non empty finite V54() set
[2,1] is non empty set
{2,1} is non empty finite V54() set
{2} is non empty trivial finite V54() 1 -element set
{{2,1},{2}} is non empty finite V54() set
[2,3] is non empty set
{2,3} is non empty finite V54() set
{{2,3},{2}} is non empty finite V54() set
[3,2] is non empty set
{3,2} is non empty finite V54() set
{3} is non empty trivial finite V54() 1 -element set
{{3,2},{3}} is non empty finite V54() set
{[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} is non empty finite set
fin_RelStr_sp is non empty Element of bool fin_RelStr
field {} is finite set
card {} is empty trivial V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite finite-yielding V54() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V71() Function-yielding V175() set
R is set
id R is Relation-like R -defined R -valued Function-like one-to-one V25(R) V29(R,R) V30(R) V31(R,R) reflexive symmetric antisymmetric transitive Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
n is set
(id R) | n is Relation-like R -defined n -defined R -defined R -valued Function-like Element of bool [:R,R:]
[:n,n:] is Relation-like set
(id R) /\ [:n,n:] is Relation-like R -defined R -valued Element of bool [:R,R:]
G is set
[:n,R:] is Relation-like set
bool [:n,R:] is non empty set
CG is set
x is set
[CG,x] is non empty set
{CG,x} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,x},{CG}} is non empty finite V54() set
G is set
CG is set
x is set
[CG,x] is non empty set
{CG,x} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,x},{CG}} is non empty finite V54() set
R is set
[R,R] is non empty set
{R,R} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,R},{R}} is non empty finite V54() set
n is set
[n,n] is non empty set
{n,n} is non empty finite set
{n} is non empty trivial finite 1 -element set
{{n,n},{n}} is non empty finite V54() set
G is set
[G,G] is non empty set
{G,G} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,G},{G}} is non empty finite V54() set
CG is set
{R,n,G,CG} is non empty finite set
id {R,n,G,CG} is non empty Relation-like {R,n,G,CG} -defined {R,n,G,CG} -valued Function-like one-to-one V25({R,n,G,CG}) V29({R,n,G,CG},{R,n,G,CG}) V30({R,n,G,CG}) V31({R,n,G,CG},{R,n,G,CG}) reflexive symmetric antisymmetric transitive finite Element of bool [:{R,n,G,CG},{R,n,G,CG}:]
[:{R,n,G,CG},{R,n,G,CG}:] is non empty Relation-like finite set
bool [:{R,n,G,CG},{R,n,G,CG}:] is non empty finite V54() set
[CG,CG] is non empty set
{CG,CG} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,CG},{CG}} is non empty finite V54() set
{[R,R],[n,n],[G,G],[CG,CG]} is non empty finite set
x is set
A is set
A is set
[A,A] is non empty set
{A,A} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,A},{A}} is non empty finite V54() set
x is set
R is set
n is set
G is set
CG is set
{R,n,G,CG} is non empty finite set
x is set
[R,x] is non empty set
{R,x} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,x},{R}} is non empty finite V54() set
[n,x] is non empty set
{n,x} is non empty finite set
{n} is non empty trivial finite 1 -element set
{{n,x},{n}} is non empty finite V54() set
[G,x] is non empty set
{G,x} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,x},{G}} is non empty finite V54() set
[CG,x] is non empty set
{CG,x} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,x},{CG}} is non empty finite V54() set
x is set
[R,x] is non empty set
{R,x} is non empty finite set
{{R,x},{R}} is non empty finite V54() set
[n,x] is non empty set
{n,x} is non empty finite set
{{n,x},{n}} is non empty finite V54() set
[G,x] is non empty set
{G,x} is non empty finite set
{{G,x},{G}} is non empty finite V54() set
[CG,x] is non empty set
{CG,x} is non empty finite set
{{CG,x},{CG}} is non empty finite V54() set
A is set
[R,A] is non empty set
{R,A} is non empty finite set
{{R,A},{R}} is non empty finite V54() set
[n,A] is non empty set
{n,A} is non empty finite set
{{n,A},{n}} is non empty finite V54() set
[G,A] is non empty set
{G,A} is non empty finite set
{{G,A},{G}} is non empty finite V54() set
[CG,A] is non empty set
{CG,A} is non empty finite set
{{CG,A},{CG}} is non empty finite V54() set
A is set
{x,x,A,A} is non empty finite set
[:{R,n,G,CG},{x,x,A,A}:] is non empty Relation-like finite set
[R,A] is non empty set
{R,A} is non empty finite set
{{R,A},{R}} is non empty finite V54() set
[n,A] is non empty set
{n,A} is non empty finite set
{{n,A},{n}} is non empty finite V54() set
{[R,x],[R,x],[n,x],[n,x],[R,A],[R,A],[n,A],[n,A]} is non empty finite set
[G,A] is non empty set
{G,A} is non empty finite set
{{G,A},{G}} is non empty finite V54() set
[CG,A] is non empty set
{CG,A} is non empty finite set
{{CG,A},{CG}} is non empty finite V54() set
{[G,x],[G,x],[CG,x],[CG,x],[G,A],[G,A],[CG,A],[CG,A]} is non empty finite set
{[R,x],[R,x],[n,x],[n,x],[R,A],[R,A],[n,A],[n,A]} \/ {[G,x],[G,x],[CG,x],[CG,x],[G,A],[G,A],[CG,A],[CG,A]} is non empty finite set
{R,n} is non empty finite set
{G,CG} is non empty finite set
{x,x} is non empty finite set
{A,A} is non empty finite set
[:{G,CG},{x,x}:] is non empty Relation-like finite set
{[G,x],[G,x],[CG,x],[CG,x]} is non empty finite set
[:{G,CG},{A,A}:] is non empty Relation-like finite set
{[G,A],[G,A],[CG,A],[CG,A]} is non empty finite set
{R,n} \/ {G,CG} is non empty finite set
{x,x} \/ {A,A} is non empty finite set
[:{R,n},{x,x}:] is non empty Relation-like finite set
[:{R,n},{A,A}:] is non empty Relation-like finite set
[:{R,n},{x,x}:] \/ [:{R,n},{A,A}:] is non empty Relation-like finite set
([:{R,n},{x,x}:] \/ [:{R,n},{A,A}:]) \/ [:{G,CG},{x,x}:] is non empty Relation-like finite set
(([:{R,n},{x,x}:] \/ [:{R,n},{A,A}:]) \/ [:{G,CG},{x,x}:]) \/ [:{G,CG},{A,A}:] is non empty Relation-like finite set
{[R,x],[R,x],[n,x],[n,x]} is non empty finite set
{[R,A],[R,A],[n,A],[n,A]} is non empty finite set
{[R,x],[R,x],[n,x],[n,x],[R,A],[R,A],[n,A],[n,A]} \/ {[G,x],[G,x],[CG,x],[CG,x]} is non empty finite set
({[R,x],[R,x],[n,x],[n,x],[R,A],[R,A],[n,A],[n,A]} \/ {[G,x],[G,x],[CG,x],[CG,x]}) \/ {[G,A],[G,A],[CG,A],[CG,A]} is non empty finite set
{[G,x],[G,x],[CG,x],[CG,x]} \/ {[G,A],[G,A],[CG,A],[CG,A]} is non empty finite set
{[R,x],[R,x],[n,x],[n,x],[R,A],[R,A],[n,A],[n,A]} \/ ({[G,x],[G,x],[CG,x],[CG,x]} \/ {[G,A],[G,A],[CG,A],[CG,A]}) is non empty finite set
R is trivial finite set
n is trivial finite set
[:R,n:] is Relation-like finite set
bool [:R,n:] is non empty finite V54() set
G is Relation-like R -defined n -valued finite Element of bool [:R,n:]
CG is set
x is set
x is set
{x} is non empty trivial finite 1 -element set
x is set
{x} is non empty trivial finite 1 -element set
x is set
{x} is non empty trivial finite 1 -element set
A is set
{A} is non empty trivial finite 1 -element set
x is set
{x} is non empty trivial finite 1 -element set
A is set
A is set
[A,A] is non empty set
{A,A} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,A},{A}} is non empty finite V54() set
R is set
{R} is non empty trivial finite 1 -element set
R is set
{R} is non empty trivial finite 1 -element set
R is set
{R} is non empty trivial finite 1 -element set
R is set
R1 is set
[R,R1] is non empty set
{R,R1} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,R1},{R}} is non empty finite V54() set
x is set
{x} is non empty trivial finite 1 -element set
A is set
{A} is non empty trivial finite 1 -element set
R is trivial finite set
[:R,R:] is Relation-like finite set
bool [:R,R:] is non empty finite V54() set
n is trivial Relation-like R -defined R -valued finite Element of bool [:R,R:]
G is set
CG is set
x is set
[CG,x] is non empty set
{CG,x} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,x},{CG}} is non empty finite V54() set
x is set
{x} is non empty trivial finite 1 -element set
[x,x] is non empty set
{x,x} is non empty finite set
{{x,x},{x}} is non empty finite V54() set
{[x,x]} is non empty trivial Relation-like Function-like one-to-one constant finite 1 -element set
A is set
A is set
R is set
[A,R] is non empty set
{A,R} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,R},{A}} is non empty finite V54() set
A is set
R is trivial finite set
[:R,R:] is Relation-like finite set
bool [:R,R:] is non empty finite V54() set
n is trivial Relation-like R -defined R -valued finite Element of bool [:R,R:]
field n is finite set
G is set
[G,G] is non empty set
{G,G} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,G},{G}} is non empty finite V54() set
G is set
[G,G] is non empty set
{G,G} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,G},{G}} is non empty finite V54() set
{[G,G]} is non empty trivial Relation-like Function-like one-to-one constant finite 1 -element set
CG is set
[CG,CG] is non empty set
{CG,CG} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,CG},{CG}} is non empty finite V54() set
dom n is trivial finite Element of bool R
bool R is non empty finite V54() set
rng n is trivial finite Element of bool R
(dom n) \/ (rng n) is trivial finite Element of bool R
G is set
CG is set
x is set
[G,CG] is non empty set
{G,CG} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,CG},{G}} is non empty finite V54() set
[CG,x] is non empty set
{CG,x} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,x},{CG}} is non empty finite V54() set
[G,x] is non empty set
{G,x} is non empty finite set
{{G,x},{G}} is non empty finite V54() set
G is set
CG is set
x is set
[G,CG] is non empty set
{G,CG} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,CG},{G}} is non empty finite V54() set
[CG,x] is non empty set
{CG,x} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,x},{CG}} is non empty finite V54() set
[G,x] is non empty set
{G,x} is non empty finite set
{{G,x},{G}} is non empty finite V54() set
x is set
[x,x] is non empty set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x},{x}} is non empty finite V54() set
{[x,x]} is non empty trivial Relation-like Function-like one-to-one constant finite 1 -element set
G is set
CG is set
[G,CG] is non empty set
{G,CG} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,CG},{G}} is non empty finite V54() set
[CG,G] is non empty set
{CG,G} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,G},{CG}} is non empty finite V54() set
G is set
CG is set
[G,CG] is non empty set
{G,CG} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,CG},{G}} is non empty finite V54() set
[CG,G] is non empty set
{CG,G} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,G},{CG}} is non empty finite V54() set
x is set
[x,x] is non empty set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x},{x}} is non empty finite V54() set
{[x,x]} is non empty trivial Relation-like Function-like one-to-one constant finite 1 -element set
dom n is trivial finite Element of bool R
bool R is non empty finite V54() set
rng n is trivial finite Element of bool R
(dom n) \/ (rng n) is trivial finite Element of bool R
G is set
CG is set
[G,CG] is non empty set
{G,CG} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,CG},{G}} is non empty finite V54() set
[CG,G] is non empty set
{CG,G} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,G},{CG}} is non empty finite V54() set
G is set
CG is set
[G,CG] is non empty set
{G,CG} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,CG},{G}} is non empty finite V54() set
[CG,G] is non empty set
{CG,G} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,G},{CG}} is non empty finite V54() set
x is set
[x,x] is non empty set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x},{x}} is non empty finite V54() set
{[x,x]} is non empty trivial Relation-like Function-like one-to-one constant finite 1 -element set
R is non empty trivial finite 1 -element set
[:R,R:] is non empty Relation-like finite set
bool [:R,R:] is non empty finite V54() set
n is trivial Relation-like R -defined R -valued reflexive symmetric strongly_connected transitive finite Element of bool [:R,R:]
G is set
{G} is non empty trivial finite 1 -element set
CG is set
x is set
[CG,x] is non empty set
{CG,x} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,x},{CG}} is non empty finite V54() set
[x,CG] is non empty set
{x,CG} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,CG},{x}} is non empty finite V54() set
{0,1} is non empty finite V54() Element of bool NAT
[0,1] is non empty Element of [:NAT,NAT:]
[1,0] is non empty Element of [:NAT,NAT:]
{[0,1],[1,0]} is non empty Relation-like NAT -defined NAT -valued finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
[:{0,1},{0,1}:] is non empty Relation-like finite set
G is set
bool [:{0,1},{0,1}:] is non empty finite V54() set
G is Relation-like {0,1} -defined {0,1} -valued finite Element of bool [:{0,1},{0,1}:]
RelStr(# {0,1},G #) is non empty strict RelStr
CG is non empty strict RelStr
the carrier of CG is non empty set
the InternalRel of CG is Relation-like the carrier of CG -defined the carrier of CG -valued Element of bool [: the carrier of CG, the carrier of CG:]
[: the carrier of CG, the carrier of CG:] is non empty Relation-like set
bool [: the carrier of CG, the carrier of CG:] is non empty set
x is set
[x,x] is non empty set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x},{x}} is non empty finite V54() set
[0,0] is non empty Element of [:NAT,NAT:]
{0,0} is non empty functional finite V54() set
{{0,0},{0}} is non empty finite V54() set
[1,1] is non empty Element of [:NAT,NAT:]
{1,1} is non empty finite V54() set
{{1,1},{1}} is non empty finite V54() set
x is set
x is set
[x,x] is non empty set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x},{x}} is non empty finite V54() set
[x,x] is non empty set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x},{x}} is non empty finite V54() set
R is irreflexive RelStr
n is full SubRelStr of R
G is set
the carrier of n is set
[G,G] is non empty set
{G,G} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,G},{G}} is non empty finite V54() 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
the carrier of R 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 Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the InternalRel of R |_2 the carrier of n is Relation-like set
the InternalRel of R /\ [: the carrier of n, the carrier of n:] is Relation-like the carrier of R -defined the carrier of R -valued set
R is symmetric RelStr
n is full SubRelStr of R
G is set
the carrier of n is set
CG is set
[G,CG] is non empty set
{G,CG} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,CG},{G}} is non empty finite V54() 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
[CG,G] is non empty set
{CG,G} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,G},{CG}} is non empty finite V54() set
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued symmetric Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the InternalRel of R |_2 the carrier of n is Relation-like set
the InternalRel of R /\ [: the carrier of n, the carrier of n:] is Relation-like the carrier of R -defined the carrier of R -valued set
R is symmetric irreflexive RelStr
the carrier of R is set
card the carrier of R is V4() V5() V6() cardinal set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued symmetric Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
G is finite set
CG is set
x is set
{CG,x} is non empty finite set
[CG,x] is non empty set
{CG} is non empty trivial finite 1 -element set
{{CG,x},{CG}} is non empty finite V54() set
[x,CG] is non empty set
{x,CG} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,CG},{x}} is non empty finite V54() set
{[CG,x],[x,CG]} is non empty Relation-like finite set
x is set
A is set
A is set
[A,A] is non empty set
{A,A} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,A},{A}} is non empty finite V54() set
[CG,CG] is non empty set
{CG,CG} is non empty finite set
{{CG,CG},{CG}} is non empty finite V54() set
[x,x] is non empty set
{x,x} is non empty finite set
{{x,x},{x}} is non empty finite V54() set
[CG,CG] is non empty set
{CG,CG} is non empty finite set
{{CG,CG},{CG}} is non empty finite V54() set
[x,x] is non empty set
{x,x} is non empty finite set
{{x,x},{x}} is non empty finite V54() set
{[CG,x]} is non empty trivial Relation-like Function-like one-to-one constant finite 1 -element set
{[x,CG]} is non empty trivial Relation-like Function-like one-to-one constant finite 1 -element set
{[CG,x]} is non empty trivial Relation-like Function-like one-to-one constant finite 1 -element set
{[x,CG]} is non empty trivial Relation-like Function-like one-to-one constant finite 1 -element set
R is non empty RelStr
n is RelStr
union_of (R,n) is strict RelStr
the carrier of R is non empty set
the carrier of n is set
the carrier of R \/ the carrier of n is non empty set
sum_of (R,n) is strict RelStr
the carrier of R is non empty set
the carrier of n is set
the carrier of R \/ the carrier of n is non empty set
R is RelStr
n is non empty RelStr
union_of (R,n) is strict RelStr
the carrier of R is set
the carrier of n is non empty set
the carrier of R \/ the carrier of n is non empty set
sum_of (R,n) is strict RelStr
the carrier of R is set
the carrier of n is non empty set
the carrier of R \/ the carrier of n is non empty set
R is finite RelStr
n is finite RelStr
union_of (R,n) is strict RelStr
the carrier of R is finite set
the carrier of n is finite set
the carrier of R \/ the carrier of n is finite set
sum_of (R,n) is strict RelStr
the carrier of R is finite set
the carrier of n is finite set
the carrier of R \/ the carrier of n is finite set
R is symmetric RelStr
n is symmetric RelStr
union_of (R,n) is strict RelStr
G is set
the carrier of (union_of (R,n)) is set
CG is set
[G,CG] is non empty set
{G,CG} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,CG},{G}} is non empty finite V54() set
the InternalRel of (union_of (R,n)) is Relation-like the carrier of (union_of (R,n)) -defined the carrier of (union_of (R,n)) -valued Element of bool [: the carrier of (union_of (R,n)), the carrier of (union_of (R,n)):]
[: the carrier of (union_of (R,n)), the carrier of (union_of (R,n)):] is Relation-like set
bool [: the carrier of (union_of (R,n)), the carrier of (union_of (R,n)):] is non empty set
[CG,G] is non empty set
{CG,G} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,G},{CG}} is non empty finite V54() set
the carrier of R is set
the carrier of n is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued symmetric Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty 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
the InternalRel of R \/ the InternalRel of n is Relation-like set
sum_of (R,n) is strict RelStr
the carrier of (sum_of (R,n)) is set
the InternalRel of (sum_of (R,n)) is Relation-like the carrier of (sum_of (R,n)) -defined the carrier of (sum_of (R,n)) -valued Element of bool [: the carrier of (sum_of (R,n)), the carrier of (sum_of (R,n)):]
[: the carrier of (sum_of (R,n)), the carrier of (sum_of (R,n)):] is Relation-like set
bool [: the carrier of (sum_of (R,n)), the carrier of (sum_of (R,n)):] is non empty set
the carrier of R is set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued symmetric Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the carrier of n is 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
R is set
R1 is set
[R,R1] is non empty set
{R,R1} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,R1},{R}} is non empty finite V54() set
[R1,R] is non empty set
{R1,R} is non empty finite set
{R1} is non empty trivial finite 1 -element set
{{R1,R},{R1}} is non empty finite V54() set
the InternalRel of R \/ the InternalRel of n is Relation-like set
[: the carrier of R, the carrier of n:] is Relation-like set
( the InternalRel of R \/ the InternalRel of n) \/ [: the carrier of R, the carrier of n:] is Relation-like set
[: the carrier of n, the carrier of R:] is Relation-like set
(( the InternalRel of R \/ the InternalRel of n) \/ [: the carrier of R, the carrier of n:]) \/ [: the carrier of n, the carrier of R:] is Relation-like set
[: the carrier of R, the carrier of n:] \/ [: the carrier of n, the carrier of R:] is Relation-like set
the InternalRel of n \/ ([: the carrier of R, the carrier of n:] \/ [: the carrier of n, the carrier of R:]) is Relation-like set
the InternalRel of n \/ [: the carrier of R, the carrier of n:] is Relation-like set
( the InternalRel of n \/ [: the carrier of R, the carrier of n:]) \/ [: the carrier of n, the carrier of R:] is Relation-like set
the InternalRel of R \/ (( the InternalRel of n \/ [: the carrier of R, the carrier of n:]) \/ [: the carrier of n, the carrier of R:]) is Relation-like set
the InternalRel of R \/ ( the InternalRel of n \/ ([: the carrier of R, the carrier of n:] \/ [: the carrier of n, the carrier of R:])) is Relation-like set
( the InternalRel of R \/ the InternalRel of n) \/ ([: the carrier of R, the carrier of n:] \/ [: the carrier of n, the carrier of R:]) is Relation-like set
[: the carrier of R, the carrier of n:] \/ [: the carrier of n, the carrier of R:] is Relation-like set
the InternalRel of n \/ ([: the carrier of R, the carrier of n:] \/ [: the carrier of n, the carrier of R:]) is Relation-like set
the InternalRel of n \/ [: the carrier of R, the carrier of n:] is Relation-like set
( the InternalRel of n \/ [: the carrier of R, the carrier of n:]) \/ [: the carrier of n, the carrier of R:] is Relation-like set
the InternalRel of R \/ (( the InternalRel of n \/ [: the carrier of R, the carrier of n:]) \/ [: the carrier of n, the carrier of R:]) is Relation-like set
the InternalRel of R \/ ( the InternalRel of n \/ ([: the carrier of R, the carrier of n:] \/ [: the carrier of n, the carrier of R:])) is Relation-like set
( the InternalRel of R \/ the InternalRel of n) \/ ([: the carrier of R, the carrier of n:] \/ [: the carrier of n, the carrier of R:]) is Relation-like set
R is irreflexive RelStr
n is irreflexive RelStr
union_of (R,n) is strict RelStr
the carrier of (union_of (R,n)) is set
the InternalRel of (union_of (R,n)) is Relation-like the carrier of (union_of (R,n)) -defined the carrier of (union_of (R,n)) -valued Element of bool [: the carrier of (union_of (R,n)), the carrier of (union_of (R,n)):]
[: the carrier of (union_of (R,n)), the carrier of (union_of (R,n)):] is Relation-like set
bool [: the carrier of (union_of (R,n)), the carrier of (union_of (R,n)):] is non empty set
the carrier of R is set
the carrier of n is set
A is set
[A,A] is non empty set
{A,A} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,A},{A}} is non empty finite V54() 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 Relation-like set
bool [: the carrier of R, the carrier of R:] 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
the InternalRel of R \/ the InternalRel of n is Relation-like set
R is irreflexive RelStr
the carrier of R is set
n is irreflexive RelStr
the carrier of n is set
sum_of (R,n) is strict RelStr
the carrier of (sum_of (R,n)) is set
the InternalRel of (sum_of (R,n)) is Relation-like the carrier of (sum_of (R,n)) -defined the carrier of (sum_of (R,n)) -valued Element of bool [: the carrier of (sum_of (R,n)), the carrier of (sum_of (R,n)):]
[: the carrier of (sum_of (R,n)), the carrier of (sum_of (R,n)):] is Relation-like set
bool [: the carrier of (sum_of (R,n)), the carrier of (sum_of (R,n)):] is non empty 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 Relation-like set
bool [: the carrier of R, the carrier of R:] 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
[: the carrier of R, the carrier of n:] is Relation-like set
[: the carrier of n, the carrier of R:] is Relation-like set
A is set
[A,A] is non empty set
{A,A} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,A},{A}} is non empty finite V54() set
the InternalRel of R \/ the InternalRel of n is Relation-like set
( the InternalRel of R \/ the InternalRel of n) \/ [: the carrier of R, the carrier of n:] is Relation-like set
(( the InternalRel of R \/ the InternalRel of n) \/ [: the carrier of R, the carrier of n:]) \/ [: the carrier of n, the carrier of R:] is Relation-like set
R is RelStr
n is RelStr
union_of (R,n) is strict RelStr
union_of (n,R) is strict RelStr
sum_of (R,n) is strict RelStr
sum_of (n,R) is strict RelStr
the carrier of (sum_of (R,n)) is set
the carrier of n is set
the carrier of R is set
the carrier of n \/ the carrier of R is set
the InternalRel of (sum_of (R,n)) is Relation-like the carrier of (sum_of (R,n)) -defined the carrier of (sum_of (R,n)) -valued Element of bool [: the carrier of (sum_of (R,n)), the carrier of (sum_of (R,n)):]
[: the carrier of (sum_of (R,n)), the carrier of (sum_of (R,n)):] is Relation-like set
bool [: the carrier of (sum_of (R,n)), the carrier of (sum_of (R,n)):] is non empty 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 Relation-like set
bool [: the carrier of R, the carrier of R:] 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 set
bool [: the carrier of n, the carrier of n:] is non empty set
the InternalRel of R \/ the InternalRel of n is Relation-like set
[: the carrier of R, the carrier of n:] is Relation-like set
( the InternalRel of R \/ the InternalRel of n) \/ [: the carrier of R, the carrier of n:] is Relation-like set
[: the carrier of n, the carrier of R:] is Relation-like set
(( the InternalRel of R \/ the InternalRel of n) \/ [: the carrier of R, the carrier of n:]) \/ [: the carrier of n, the carrier of R:] is Relation-like set
the InternalRel of n \/ the InternalRel of R is Relation-like set
( the InternalRel of n \/ the InternalRel of R) \/ [: the carrier of n, the carrier of R:] is Relation-like set
(( the InternalRel of n \/ the InternalRel of R) \/ [: the carrier of n, the carrier of R:]) \/ [: the carrier of R, the carrier of n:] is Relation-like set
the carrier of (union_of (R,n)) is set
the InternalRel of (union_of (R,n)) is Relation-like the carrier of (union_of (R,n)) -defined the carrier of (union_of (R,n)) -valued Element of bool [: the carrier of (union_of (R,n)), the carrier of (union_of (R,n)):]
[: the carrier of (union_of (R,n)), the carrier of (union_of (R,n)):] is Relation-like set
bool [: the carrier of (union_of (R,n)), the carrier of (union_of (R,n)):] is non empty set
R is irreflexive RelStr
n is RelStr
G is RelStr
union_of (n,G) is strict RelStr
sum_of (n,G) is strict RelStr
the carrier of n is set
the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
CG is set
[CG,CG] is non empty set
{CG,CG} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,CG},{CG}} is non empty finite V54() set
the InternalRel of G is Relation-like the carrier of G -defined the carrier of G -valued Element of bool [: the carrier of G, the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is Relation-like set
bool [: the carrier of G, the carrier of G:] is non empty set
the InternalRel of n \/ the InternalRel of G is Relation-like 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 is set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the carrier of n \/ the carrier of G is set
the carrier of G is set
the InternalRel of G is Relation-like the carrier of G -defined the carrier of G -valued Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
bool [: the carrier of G, the carrier of G:] is non empty set
CG is set
[CG,CG] is non empty set
{CG,CG} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,CG},{CG}} is non empty finite V54() 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
the InternalRel of n \/ the InternalRel of G is Relation-like 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 is set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the carrier of n \/ the carrier of G is set
the carrier of n is set
the InternalRel of n is Relation-like the carrier of n -defined the carrier of n -valued Element of bool [: the carrier of n, the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
CG is set
[CG,CG] is non empty set
{CG,CG} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,CG},{CG}} is non empty finite V54() set
the InternalRel of G is Relation-like the carrier of G -defined the carrier of G -valued Element of bool [: the carrier of G, the carrier of G:]
the carrier of G is set
[: the carrier of G, the carrier of G:] is Relation-like set
bool [: the carrier of G, the carrier of G:] is non empty set
the InternalRel of n \/ the InternalRel of G is Relation-like set
[: the carrier of n, the carrier of G:] is Relation-like set
( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:] is Relation-like set
[: the carrier of G, the carrier of n:] is Relation-like set
(( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:] is Relation-like 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 is set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the carrier of n \/ the carrier of G is set
the carrier of G is set
the InternalRel of G is Relation-like the carrier of G -defined the carrier of G -valued Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
bool [: the carrier of G, the carrier of G:] is non empty set
CG is set
[CG,CG] is non empty set
{CG,CG} is non empty finite set
{CG} is non empty trivial finite 1 -element set
{{CG,CG},{CG}} is non empty finite V54() 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
the InternalRel of n \/ the InternalRel of G is Relation-like set
[: the carrier of n, the carrier of G:] is Relation-like set
( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:] is Relation-like set
[: the carrier of G, the carrier of n:] is Relation-like set
(( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:] is Relation-like 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 is set
[: the carrier of R, the carrier of R:] is Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
the carrier of n \/ the carrier of G is set
R is non empty RelStr
the carrier of R is non empty 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 non empty Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty set
RelStr(# the carrier of R, the InternalRel of R #) is non empty strict RelStr
n is RelStr
the carrier of n is set
G is RelStr
the carrier of G is set
union_of (n,G) is strict RelStr
sum_of (n,G) 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, the carrier of n:] is Relation-like set
bool [: the carrier of n, the carrier of n:] is non empty set
the InternalRel of G is Relation-like the carrier of G -defined the carrier of G -valued Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
bool [: the carrier of G, the carrier of G:] is non empty set
[: the carrier of n, the carrier of G:] is Relation-like set
[: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of R |_2 the carrier of G is Relation-like set
the InternalRel of R /\ [: the carrier of G, the carrier of G:] is Relation-like the carrier of R -defined the carrier of R -valued set
R is set
the InternalRel of n \/ the InternalRel of G is Relation-like set
R is set
the InternalRel of n \/ the InternalRel of G is Relation-like set
R1 is set
R2 is set
[R1,R2] is non empty set
{R1,R2} is non empty finite set
{R1} is non empty trivial finite 1 -element set
{{R1,R2},{R1}} is non empty finite V54() set
R22 is set
R11 is set
[R22,R11] is non empty set
{R22,R11} is non empty finite set
{R22} is non empty trivial finite 1 -element set
{{R22,R11},{R22}} is non empty finite V54() set
the carrier of n /\ the carrier of G is set
the InternalRel of R |_2 the carrier of n is Relation-like set
the InternalRel of R /\ [: the carrier of n, the carrier of n:] is Relation-like the carrier of R -defined the carrier of R -valued set
R is set
the InternalRel of n \/ the InternalRel of G is Relation-like set
R is set
the InternalRel of n \/ the InternalRel of G is Relation-like set
R1 is set
R2 is set
[R1,R2] is non empty set
{R1,R2} is non empty finite set
{R1} is non empty trivial finite 1 -element set
{{R1,R2},{R1}} is non empty finite V54() set
R22 is set
R11 is set
[R22,R11] is non empty set
{R22,R11} is non empty finite set
{R22} is non empty trivial finite 1 -element set
{{R22,R11},{R22}} is non empty finite V54() set
the carrier of n \/ the carrier of G is set
the InternalRel of n \/ the InternalRel of G is Relation-like set
the InternalRel of R |_2 the carrier of G is Relation-like set
the InternalRel of R /\ [: the carrier of G, the carrier of G:] is Relation-like the carrier of R -defined the carrier of R -valued set
R is set
the InternalRel of n \/ the InternalRel of G is Relation-like set
( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:] is Relation-like set
(( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of n \/ [: the carrier of n, the carrier of G:] is Relation-like set
( the InternalRel of n \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of G \/ (( the InternalRel of n \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:]) is Relation-like set
R is set
the InternalRel of n \/ the InternalRel of G is Relation-like set
( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:] is Relation-like set
(( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of G \/ [: the carrier of n, the carrier of G:] is Relation-like set
( the InternalRel of G \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of n \/ (( the InternalRel of G \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:]) is Relation-like set
[: the carrier of n, the carrier of G:] \/ [: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of G \/ ([: the carrier of n, the carrier of G:] \/ [: the carrier of G, the carrier of n:]) is Relation-like set
R1 is set
R2 is set
[R1,R2] is non empty set
{R1,R2} is non empty finite set
{R1} is non empty trivial finite 1 -element set
{{R1,R2},{R1}} is non empty finite V54() set
R22 is set
R11 is set
[R22,R11] is non empty set
{R22,R11} is non empty finite set
{R22} is non empty trivial finite 1 -element set
{{R22,R11},{R22}} is non empty finite V54() set
the carrier of n /\ the carrier of G is set
R1 is set
R2 is set
[R1,R2] is non empty set
{R1,R2} is non empty finite set
{R1} is non empty trivial finite 1 -element set
{{R1,R2},{R1}} is non empty finite V54() set
R22 is set
R11 is set
[R22,R11] is non empty set
{R22,R11} is non empty finite set
{R22} is non empty trivial finite 1 -element set
{{R22,R11},{R22}} is non empty finite V54() set
the carrier of n /\ the carrier of G is set
R1 is set
R2 is set
[R1,R2] is non empty set
{R1,R2} is non empty finite set
{R1} is non empty trivial finite 1 -element set
{{R1,R2},{R1}} is non empty finite V54() set
R22 is set
R11 is set
[R22,R11] is non empty set
{R22,R11} is non empty finite set
{R22} is non empty trivial finite 1 -element set
{{R22,R11},{R22}} is non empty finite V54() set
the carrier of n /\ the carrier of G is set
the InternalRel of n \/ the InternalRel of G is Relation-like set
( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:] is Relation-like set
(( the InternalRel of n \/ the InternalRel of G) \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of R |_2 the carrier of n is Relation-like set
the InternalRel of R /\ [: the carrier of n, the carrier of n:] is Relation-like the carrier of R -defined the carrier of R -valued set
R is set
the InternalRel of G \/ [: the carrier of n, the carrier of G:] is Relation-like set
( the InternalRel of G \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of n \/ (( the InternalRel of G \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:]) is Relation-like set
R is set
the InternalRel of G \/ [: the carrier of n, the carrier of G:] is Relation-like set
( the InternalRel of G \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of n \/ (( the InternalRel of G \/ [: the carrier of n, the carrier of G:]) \/ [: the carrier of G, the carrier of n:]) is Relation-like set
[: the carrier of n, the carrier of G:] \/ [: the carrier of G, the carrier of n:] is Relation-like set
the InternalRel of G \/ ([: the carrier of n, the carrier of G:] \/ [: the carrier of G, the carrier of n:]) is Relation-like set
R1 is set
R2 is set
[R1,R2] is non empty set
{R1,R2} is non empty finite set
{R1} is non empty trivial finite 1 -element set
{{R1,R2},{R1}} is non empty finite V54() set
R22 is set
R11 is set
[R22,R11] is non empty set
{R22,R11} is non empty finite set
{R22} is non empty trivial finite 1 -element set
{{R22,R11},{R22}} is non empty finite V54() set
the carrier of n /\ the carrier of G is set
R1 is set
R2 is set
[R1,R2] is non empty set
{R1,R2} is non empty finite set
{R1} is non empty trivial finite 1 -element set
{{R1,R2},{R1}} is non empty finite V54() set
R22 is set
R11 is set
[R22,R11] is non empty set
{R22,R11} is non empty finite set
{R22} is non empty trivial finite 1 -element set
{{R22,R11},{R22}} is non empty finite V54() set
the carrier of n /\ the carrier of G is set
R1 is set
R2 is set
[R1,R2] is non empty set
{R1,R2} is non empty finite set
{R1} is non empty trivial finite 1 -element set
{{R1,R2},{R1}} is non empty finite V54() set
R22 is set
R11 is set
[R22,R11] is non empty set
{R22,R11} is non empty finite set
{R22} is non empty trivial finite 1 -element set
{{R22,R11},{R22}} is non empty finite V54() set
the carrier of n /\ the carrier of G is set
the InternalRel of G \/ [: the carrier of n, the carrier of G:] is Relation-like set
the InternalRel of n \/ ( the InternalRel of G \/ [: the carrier of n, the carrier of G:]) is Relation-like set
the carrier of n \/ the carrier of G is set
the InternalRel of (ComplRelStr (Necklace 4)) is Relation-like the carrier of (ComplRelStr (Necklace 4)) -defined the carrier of (ComplRelStr (Necklace 4)) -valued Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (ComplRelStr (Necklace 4)):]
the carrier of (ComplRelStr (Necklace 4)) is non empty set
[: the carrier of (ComplRelStr (Necklace 4)), the carrier of (ComplRelStr (Necklace 4)):] is non empty Relation-like set
bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (ComplRelStr (Necklace 4)):] is non empty set
[0,2] is non empty Element of [:NAT,NAT:]
{0,2} is non empty finite V54() set
{{0,2},{0}} is non empty finite V54() set
[2,0] is non empty Element of [:NAT,NAT:]
{2,0} is non empty finite V54() set
{{2,0},{2}} is non empty finite V54() set
[0,3] is non empty Element of [:NAT,NAT:]
{0,3} is non empty finite V54() set
{{0,3},{0}} is non empty finite V54() set
[3,0] is non empty Element of [:NAT,NAT:]
{3,0} is non empty finite V54() set
{{3,0},{3}} is non empty finite V54() set
[1,3] is non empty Element of [:NAT,NAT:]
{1,3} is non empty finite V54() set
{{1,3},{1}} is non empty finite V54() set
[3,1] is non empty Element of [:NAT,NAT:]
{3,1} is non empty finite V54() set
{{3,1},{3}} is non empty finite V54() set
{[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} is non empty Relation-like NAT -defined NAT -valued finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
{0,1,2,3} is non empty finite Element of bool NAT
CG is set
the InternalRel of (Necklace 4) ` is Relation-like the carrier of (Necklace 4) -defined the carrier of (Necklace 4) -valued finite Element of bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):]
id the carrier of (Necklace 4) is non empty Relation-like the carrier of (Necklace 4) -defined the carrier of (Necklace 4) -valued Function-like one-to-one V25( the carrier of (Necklace 4)) V29( the carrier of (Necklace 4), the carrier of (Necklace 4)) V30( the carrier of (Necklace 4)) V31( the carrier of (Necklace 4), the carrier of (Necklace 4)) reflexive symmetric antisymmetric transitive finite Element of bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):]
( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) is Relation-like the carrier of (Necklace 4) -defined the carrier of (Necklace 4) -valued finite Element of bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):]
[: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) is Relation-like the carrier of (Necklace 4) -defined the carrier of (Necklace 4) -valued finite Element of bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):]
x is set
x is set
[x,x] is non empty set
{x,x} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,x},{x}} is non empty finite V54() set
CG is set
[0,1] is non empty Element of [:NAT,NAT:]
[1,0] is non empty Element of [:NAT,NAT:]
[1,2] is non empty Element of [:NAT,NAT:]
[2,1] is non empty Element of [:NAT,NAT:]
[2,3] is non empty Element of [:NAT,NAT:]
[3,2] is non empty Element of [:NAT,NAT:]
[0,1] is non empty Element of [:NAT,NAT:]
[1,0] is non empty Element of [:NAT,NAT:]
[1,2] is non empty Element of [:NAT,NAT:]
[2,1] is non empty Element of [:NAT,NAT:]
[2,3] is non empty Element of [:NAT,NAT:]
[3,2] is non empty Element of [:NAT,NAT:]
[: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) is Relation-like the carrier of (Necklace 4) -defined the carrier of (Necklace 4) -valued finite Element of bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):]
the InternalRel of (Necklace 4) ` is Relation-like the carrier of (Necklace 4) -defined the carrier of (Necklace 4) -valued finite Element of bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):]
id the carrier of (Necklace 4) is non empty Relation-like the carrier of (Necklace 4) -defined the carrier of (Necklace 4) -valued Function-like one-to-one V25( the carrier of (Necklace 4)) V29( the carrier of (Necklace 4), the carrier of (Necklace 4)) V30( the carrier of (Necklace 4)) V31( the carrier of (Necklace 4), the carrier of (Necklace 4)) reflexive symmetric antisymmetric transitive finite Element of bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):]
( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) is Relation-like the carrier of (Necklace 4) -defined the carrier of (Necklace 4) -valued finite Element of bool [: the carrier of (Necklace 4), the carrier of (Necklace 4):]
[0,1] is non empty Element of [:NAT,NAT:]
[1,0] is non empty Element of [:NAT,NAT:]
[1,2] is non empty Element of [:NAT,NAT:]
[2,1] is non empty Element of [:NAT,NAT:]
[2,3] is non empty Element of [:NAT,NAT:]
[3,2] is non empty Element of [:NAT,NAT