:: 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
is non empty non trivial Relation-like non finite set
is non empty non trivial Relation-like non finite set
bool 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

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,1,2,3} is non empty finite set

ComplRelStr () is non empty strict RelStr
FinSETS is non empty universal set
K139({}) is set
the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued symmetric finite Element of bool [: the carrier of (), the carrier of ():]
the carrier of () is non empty finite set
[: the carrier of (), the carrier of ():] is non empty Relation-like finite set
bool [: the carrier of (), the carrier of ():] is non empty finite V54() set
[0,1] is non empty set
{0,1} is non empty finite V54() set
is non empty trivial functional finite V54() 1 -element set
{{0,1},} 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

R is set

[:R,R:] is Relation-like set
bool [:R,R:] is non empty set
n is set

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

bool [:R,n:] is non empty finite V54() set

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

bool [:R,R:] 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
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

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

bool [:R,R:] 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 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
[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

bool R is non empty finite V54() set

(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

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

bool R is non empty finite V54() set

(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

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

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
[1,0] is non empty Element of

bool 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

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
{0,0} is non empty functional finite V54() set
is non empty finite V54() set
[1,1] is non empty Element of
{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

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

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

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

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

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

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

the carrier of R is set

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

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 () is Relation-like the carrier of () -defined the carrier of () -valued Element of bool [: the carrier of (), the carrier of ():]
the carrier of () is non empty set
[: the carrier of (), the carrier of ():] is non empty Relation-like set
bool [: the carrier of (), the carrier of ():] is non empty set
[0,2] is non empty Element of
{0,2} is non empty finite V54() set
{{0,2},} is non empty finite V54() set
[2,0] is non empty Element of
{2,0} is non empty finite V54() set
{{2,0},{2}} is non empty finite V54() set
[0,3] is non empty Element of
{0,3} is non empty finite V54() set
{{0,3},} is non empty finite V54() set
[3,0] is non empty Element of
{3,0} is non empty finite V54() set
{{3,0},{3}} is non empty finite V54() set
[1,3] is non empty Element of
{1,3} is non empty finite V54() set
{{1,3},{1}} is non empty finite V54() set
[3,1] is non empty Element of
{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
bool 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 () ` is Relation-like the carrier of () -defined the carrier of () -valued finite Element of bool [: the carrier of (), the carrier of ():]
id the carrier of () is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like one-to-one V25( the carrier of ()) V29( the carrier of (), the carrier of ()) V30( the carrier of ()) V31( the carrier of (), the carrier of ()) reflexive symmetric antisymmetric transitive finite Element of bool [: the carrier of (), the carrier of ():]
( the InternalRel of () `) \ (id the carrier of ()) is Relation-like the carrier of () -defined the carrier of () -valued finite Element of bool [: the carrier of (), the carrier of ():]
[: the carrier of (), the carrier of ():] \ the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued finite Element of bool [: the carrier of (), the carrier of ():]
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
[1,0] is non empty Element of
[1,2] is non empty Element of
[2,1] is non empty Element of
[2,3] is non empty Element of
[3,2] is non empty Element of
[0,1] is non empty Element of
[1,0] is non empty Element of
[1,2] is non empty Element of
[2,1] is non empty Element of
[2,3] is non empty Element of
[3,2] is non empty Element of
[: the carrier of (), the carrier of ():] \ the InternalRel of () is Relation-like the carrier of () -defined the carrier of () -valued finite Element of bool [: the carrier of (), the carrier of ():]
the InternalRel of () ` is Relation-like the carrier of () -defined the carrier of () -valued finite Element of bool [: the carrier of (), the carrier of ():]
id the carrier of () is non empty Relation-like the carrier of () -defined the carrier of () -valued Function-like one-to-one V25( the carrier of ()) V29( the carrier of (), the carrier of ()) V30( the carrier of ()) V31( the carrier of (), the carrier of ()) reflexive symmetric antisymmetric transitive finite Element of bool [: the carrier of (), the carrier of ():]
( the InternalRel of () `) \ (id the carrier of ()) is Relation-like the carrier of () -defined the carrier of () -valued finite Element of bool [: the carrier of (), the carrier of ():]
[0,1] is non empty Element of
[1,0] is non empty Element of
[1,2] is non empty Element of
[2,1] is non empty Element of
[2,3] is non empty Element of
[3,2] is non empty Element of