:: NECKLA_3 semantic presentation

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