:: GRAPH_1 semantic presentation

REAL is set

NAT is non empty non trivial V25() V26() V27() non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

NAT is non empty non trivial V25() V26() V27() 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

1 is non empty ext-real positive V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

[:1,1:] is Relation-like non empty finite set

bool [:1,1:] is non empty finite V37() set

[:[:1,1:],1:] is Relation-like non empty finite set

bool [:[:1,1:],1:] is non empty finite V37() set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V24() V25() V26() V27() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

2 is non empty ext-real positive V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

3 is non empty ext-real positive V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V24() V25() V26() V27() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

op1 is Relation-like 1 -defined 1 -valued Function-like non empty total quasi_total finite Element of bool [:1,1:]

(1,1,op1,op1) is () ()

G1 is ()

the carrier' of G1 is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier of G1 is set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

G is Element of the carrier' of G1

the of G1 . G is set

the Element of the carrier of G1 is Element of the carrier of G1

G2 is non empty non void feasible ()

the carrier' of G2 is non empty set

the carrier of G2 is non empty set

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

[: the carrier' of G2, the carrier of G2:] is Relation-like non empty set

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

G is Element of the carrier' of G2

the of G2 . G is Element of the carrier of G2

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the of G1 . G is set

G2 is non empty non void feasible ()

the carrier' of G2 is non empty set

the carrier of G2 is non empty set

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

[: the carrier' of G2, the carrier of G2:] is Relation-like non empty set

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

G is Element of the carrier' of G2

the of G2 . G is Element of the carrier of G2

G1 is non empty non void feasible ()

the carrier' of G1 is non empty set

the carrier of G1 is non empty set

G is Element of the carrier' of G1

(G1,G) is Element of the carrier of G1

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like non empty set

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

the of G1 . G is Element of the carrier of G1

G2 is Element of the carrier of G1

G is Element of the carrier of G1

(G1,G) is Element of the carrier of G1

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the of G1 . G is Element of the carrier of G1

G2 is Element of the carrier of G1

G is Element of the carrier of G1

G1 is non empty feasible ()

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier' of G1 is set

the carrier of G1 is non empty set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

G is non empty feasible ()

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier' of G is set

the carrier of G is non empty 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 of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier of G1 \/ the carrier of G is non empty set

the carrier' of G1 \/ the carrier' of G is set

[:( the carrier' of G1 \/ the carrier' of G),( the carrier of G1 \/ the carrier of G):] is Relation-like set

bool [:( the carrier' of G1 \/ the carrier' of G),( the carrier of G1 \/ the carrier of G):] is non empty set

v is set

the of G1 . v is set

the of G . v is set

G2 is set

the carrier' of G1 /\ the carrier' of G is set

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

(dom the of G1) /\ (dom the of G) is Element of bool the carrier' of G

G2 is set

G2 is set

v is set

v is Relation-like the carrier' of G1 \/ the carrier' of G -defined the carrier of G1 \/ the carrier of G -valued Function-like total quasi_total Element of bool [:( the carrier' of G1 \/ the carrier' of G),( the carrier of G1 \/ the carrier of G):]

G2 is set

v . G2 is set

the of G1 . G2 is set

G2 is set

v . G2 is set

the of G . G2 is set

v is Relation-like the carrier' of G1 \/ the carrier' of G -defined the carrier of G1 \/ the carrier of G -valued Function-like total quasi_total Element of bool [:( the carrier' of G1 \/ the carrier' of G),( the carrier of G1 \/ the carrier of G):]

v is Relation-like the carrier' of G1 \/ the carrier' of G -defined the carrier of G1 \/ the carrier of G -valued Function-like total quasi_total Element of bool [:( the carrier' of G1 \/ the carrier' of G),( the carrier of G1 \/ the carrier of G):]

G2 is set

the of G1 . G2 is set

the of G . G2 is set

v is set

the carrier' of G1 /\ the carrier' of G is set

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

(dom the of G1) /\ (dom the of G) is Element of bool the carrier' of G

v is set

v is set

T2 is set

G2 is Relation-like the carrier' of G1 \/ the carrier' of G -defined the carrier of G1 \/ the carrier of G -valued Function-like total quasi_total Element of bool [:( the carrier' of G1 \/ the carrier' of G),( the carrier of G1 \/ the carrier of G):]

v is set

G2 . v is set

the of G1 . v is set

v is set

G2 . v is set

the of G . v is set

G2 is Relation-like the carrier' of G1 \/ the carrier' of G -defined the carrier of G1 \/ the carrier of G -valued Function-like total quasi_total Element of bool [:( the carrier' of G1 \/ the carrier' of G),( the carrier of G1 \/ the carrier of G):]

G2 is Relation-like the carrier' of G1 \/ the carrier' of G -defined the carrier of G1 \/ the carrier of G -valued Function-like total quasi_total Element of bool [:( the carrier' of G1 \/ the carrier' of G),( the carrier of G1 \/ the carrier of G):]

(( the carrier of G1 \/ the carrier of G),( the carrier' of G1 \/ the carrier' of G),v,G2) is () ()

v is non empty feasible () ()

the carrier of v is non empty set

the carrier' of v is set

the of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like total quasi_total Element of bool [: the carrier' of v, the carrier of v:]

[: the carrier' of v, the carrier of v:] is Relation-like set

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

the of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like total quasi_total Element of bool [: the carrier' of v, the carrier of v:]

T2 is set

the of v . T2 is set

the of G1 . T2 is set

the of v . T2 is set

the of G1 . T2 is set

T2 is set

the of v . T2 is set

the of G . T2 is set

the of v . T2 is set

the of G . T2 is set

G2 is non empty feasible () ()

the carrier of G2 is non empty set

the carrier' of G2 is set

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

[: the carrier' of G2, the carrier of G2:] is Relation-like set

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

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

G is non empty feasible () ()

the carrier of G is non empty set

the carrier' of G is set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total 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 of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

dom the of G2 is Element of bool the carrier' of G2

bool the carrier' of G2 is non empty set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

dom the of G2 is Element of bool the carrier' of G2

dom the of G is Element of bool the carrier' of G

v is set

the of G2 . v is set

the of G . v is set

the of G1 . v is set

the of G . v is set

v is set

the of G2 . v is set

the of G . v is set

the of G1 . v is set

the of G . v is set

op1 is Relation-like 1 -defined 1 -valued Function-like non empty total quasi_total finite Element of bool [:1,1:]

(1,1,op1,op1) is () ()

G1 is () ()

the carrier of G1 is set

the carrier' of G1 is set

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

[:{},{1}:] is Relation-like finite set

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

G is Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional empty total quasi_total ext-real V24() V25() V26() V27() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},{1}:]

({1},{},G,G) is () ()

G2 is non empty feasible ()

the carrier' of G2 is set

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

the carrier of G2 is non empty set

[: the carrier' of G2, the carrier of G2:] is Relation-like set

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

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

G is set

v is set

the of G2 . G is set

the of G2 . v is set

the of G2 . G is set

the of G2 . v is set

G is set

v is set

the of G2 . G is set

the of G2 . v is set

the of G2 . G is set

the of G2 . v is set

G is set

the of G2 . G is set

the of G2 . G is set

G is non empty feasible ()

the carrier of G is non empty set

v is non empty feasible ()

the carrier of v is non empty set

the carrier of G /\ the carrier of v is set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total 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 of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like total quasi_total Element of bool [: the carrier' of v, the carrier of v:]

the carrier' of v is set

[: the carrier' of v, the carrier of v:] is Relation-like set

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

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like total quasi_total Element of bool [: the carrier' of v, the carrier of v:]

(G,v) is non empty feasible () ()

the carrier of G \/ the carrier of v is non empty set

the Element of the carrier of G is Element of the carrier of G

the Element of the carrier of v is Element of the carrier of v

G1 is () ()

the carrier of G1 is set

the carrier' of G1 is set

G1 is non empty feasible ()

the carrier of G1 is non empty set

G1 is non empty feasible ()

the carrier of G1 is non empty set

G1 is non empty feasible ()

the carrier' of G1 is set

the carrier of G1 is non empty set

len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V24() V25() V26() V27() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

(len {}) + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

{} . G is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V24() V25() V26() V27() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

the Element of the carrier of G1 is Element of the carrier of G1

<* the Element of the carrier of G1*> is Relation-like NAT -defined the carrier of G1 -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G1

len <* the Element of the carrier of G1*> is non empty ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . G2 is set

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . G2 is set

G2 + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . (G2 + 1) is set

{} . G2 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V24() V25() V26() V27() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

G1 is non empty feasible ()

len {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V24() V25() V26() V27() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

the carrier' of G1 is set

G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

{} . G is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V24() V25() V26() V27() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

(len {}) + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

the carrier of G1 is non empty set

the Element of the carrier of G1 is Element of the carrier of G1

<* the Element of the carrier of G1*> is Relation-like NAT -defined the carrier of G1 -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G1

len <* the Element of the carrier of G1*> is non empty ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . G2 is set

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . G2 is set

G2 + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . (G2 + 1) is set

{} . G2 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real V24() V25() V26() V27() V29() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

G1 is non empty feasible ()

the carrier' of G1 is set

G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like (G1)

rng G is finite set

G2 is set

dom G is finite Element of bool NAT

G is set

G . G is set

v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

len G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G1 is non empty feasible ()

the carrier' of G1 is set

G1 is non empty feasible ()

the carrier' of G1 is set

G1 is non empty feasible ()

the carrier' of G1 is set

G is Relation-like NAT -defined the carrier' of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

len G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier of G1 is non empty set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

G2 + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G . (G2 + 1) is set

the of G1 . (G . (G2 + 1)) is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

G . G2 is set

the of G1 . (G . G2) is set

G1 is non empty feasible ()

the carrier' of G1 is set

G is Relation-like NAT -defined the carrier' of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G . G2 is set

G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G . G is set

dom G is finite Element of bool NAT

G2 is set

dom G is finite set

G is set

G . G2 is set

G . G is set

dom G is finite Element of bool NAT

v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G1 is non empty feasible ()

the carrier' of G1 is set

G1 is non empty feasible ()

the carrier' of G1 is set

G is Relation-like NAT -defined the carrier' of G1 -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like (G1)

the carrier of G1 is non empty set

the Element of the carrier of G1 is Element of the carrier of G1

<* the Element of the carrier of G1*> is Relation-like NAT -defined the carrier of G1 -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of G1

len <* the Element of the carrier of G1*> is non empty ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

len G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

(len G) + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . 1 is set

<* the Element of the carrier of G1*> . (len <* the Element of the carrier of G1*>) is set

G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . G is set

G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . G is set

G + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

<* the Element of the carrier of G1*> . (G + 1) is set

G . G is set

G1 is non empty feasible ()

the carrier of G1 is non empty set

the carrier' of G1 is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

G is set

the of G1 . G is set

the of G1 . G is set

G1 is non empty feasible ()

the carrier of G1 is non empty set

the carrier' of G1 is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

( the carrier of G1, the carrier' of G1, the of G1, the of G1) is () ()

G is non empty feasible ()

the carrier' of G is set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier of G is non empty 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 of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

G2 is set

the of G . G2 is set

the of G1 . G2 is set

the of G . G2 is set

the of G1 . G2 is set

G1 is non empty feasible () ()

the carrier of G1 is non empty finite set

card the carrier of G1 is non empty ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G is finite set

G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

card G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is finite set

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

card v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

the carrier' of G1 is finite set

card the carrier' of G1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G is finite set

G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

card G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is finite set

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

card v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G1 is non empty feasible () ()

the carrier of G1 is non empty finite set

the carrier' of G1 is finite set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total finite Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like finite set

bool [: the carrier' of G1, the carrier of G1:] is non empty finite V37() set

G is Element of the carrier of G1

G2 is set

G is set

G is finite set

card G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is set

the of G1 . v is set

G2 is set

the of G1 . G2 is set

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is finite set

card v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is finite set

card v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 is finite set

card G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 is finite set

card G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is set

the of G1 . v is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total finite Element of bool [: the carrier' of G1, the carrier of G1:]

G2 is set

G is set

G is finite set

card G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is set

the of G1 . v is set

G2 is set

the of G1 . G2 is set

G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is finite set

card v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is finite set

card v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 is finite set

card G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 is finite set

card G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is set

the of G1 . v is set

G1 is non empty feasible () ()

the carrier of G1 is non empty finite set

G is Element of the carrier of G1

(G1,G) is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

(G1,G) is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

(G1,G) + (G1,G) is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

Seg G1 is finite G1 -element Element of bool NAT

G is non empty feasible ()

the carrier' of G is set

G2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like (G)

G2 | (Seg G1) is Relation-like NAT -defined Seg G1 -defined NAT -defined the carrier' of G -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier' of G:]

[:NAT, the carrier' of G:] is Relation-like set

bool [:NAT, the carrier' of G:] is non empty set

G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len G is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G . v is set

dom G is finite Element of bool NAT

dom G2 is finite Element of bool NAT

len G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 . v is set

(len G) + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

the carrier of G is non empty set

len G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

(len G2) + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G1 + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

Seg (G1 + 1) is finite G1 + 1 -element Element of bool NAT

v | (Seg (G1 + 1)) is Relation-like NAT -defined Seg (G1 + 1) -defined NAT -defined Function-like finite FinSubsequence-like set

G2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len G2 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

dom G2 is finite Element of bool NAT

dom v is finite Element of bool NAT

(dom v) /\ (Seg (G1 + 1)) is finite Element of bool NAT

Seg ((len G2) + 1) is finite (len G2) + 1 -element Element of bool NAT

(Seg ((len G2) + 1)) /\ (Seg (G1 + 1)) is finite Element of bool NAT

dom G is finite Element of bool NAT

dom G2 is finite Element of bool NAT

(dom G2) /\ (Seg G1) is finite Element of bool NAT

Seg (len G2) is finite len G2 -element Element of bool NAT

(Seg (len G2)) /\ (Seg G1) is finite Element of bool NAT

v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 . v is set

dom G2 is finite Element of bool NAT

dom v is finite Element of bool NAT

v . v is set

v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 . v is set

v + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G2 . (v + 1) is set

G . v is set

dom G is finite Element of bool NAT

dom G2 is finite Element of bool NAT

v . v is set

v . (v + 1) is set

G2 . v is set

T2 is Element of the carrier of G

v is Element of the carrier of G

dom G2 is finite Element of bool NAT

1 + 1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len v is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

G1 is non empty feasible ()

G is non empty feasible () (G1)

the carrier of G is non empty set

G2 is non empty feasible () (G1)

the carrier of G2 is non empty set

the carrier' of G is set

the carrier' of G2 is set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total 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

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

[: the carrier' of G2, the carrier of G2:] is Relation-like set

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

dom the of G2 is Element of bool the carrier' of G2

bool the carrier' of G2 is non empty set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

dom the of G is Element of bool the carrier' of G

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

dom the of G2 is Element of bool the carrier' of G2

G is set

the of G . G is set

the of G2 . G is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier' of G1 is set

the carrier of G1 is non empty set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 . G is set

G is set

the of G . G is set

the of G2 . G is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier' of G1 is set

the carrier of G1 is non empty set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 . G is set

G2 is non empty feasible ()

the carrier' of G2 is set

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

the carrier of G2 is non empty set

[: the carrier' of G2, the carrier of G2:] is Relation-like set

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

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

G is set

the of G2 . G is set

the of G2 . G is set

G1 is non empty feasible ()

the carrier' of G1 is set

the carrier of G1 is non empty set

PFuncs ( the carrier' of G1, the carrier of G1) is functional non empty set

G is non empty feasible (G1)

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier' of G is set

the carrier of G is non empty 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 of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

Funcs ( the carrier' of G, the carrier of G) is functional non empty FUNCTION_DOMAIN of the carrier' of G, the carrier of G

PFuncs ( the carrier' of G, the carrier of G) is functional non empty set

G1 is non empty feasible ()

the carrier of G1 is non empty set

the carrier' of G1 is set

G is non empty set

bool G is non empty set

bool the carrier' of G1 is non empty set

PFuncs ( the carrier' of G1,G) is functional non empty set

[:(bool G),(bool the carrier' of G1),(PFuncs ( the carrier' of G1,G)),(PFuncs ( the carrier' of G1,G)):] is non empty set

v is set

e is set

y is non empty set

[:e,y:] is Relation-like set

bool [:e,y:] is non empty set

c

c

[:c

bool [:c

v is Element of [:(bool G),(bool the carrier' of G1),(PFuncs ( the carrier' of G1,G)),(PFuncs ( the carrier' of G1,G)):]

G2 is set

v `1_4 is Element of bool G

v `1 is set

(v `1) `1 is set

((v `1) `1) `1 is set

v `2_4 is Element of bool the carrier' of G1

((v `1) `1) `2 is set

s is Relation-like e -defined y -valued Function-like total quasi_total Element of bool [:e,y:]

v `3_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)

(v `1) `2 is set

t is Relation-like e -defined y -valued Function-like total quasi_total Element of bool [:e,y:]

v `4_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)

x is non empty feasible () ()

(y,e,s,t) is () ()

v is set

c

c

c

(c

((c

c

((c

c

c

(c

c

c

c

(c

T2 is set

G2 is set

v is set

e is set

y is non empty set

[:e,y:] is Relation-like set

bool [:e,y:] is non empty set

T2 is set

v is Element of [:(bool G),(bool the carrier' of G1),(PFuncs ( the carrier' of G1,G)),(PFuncs ( the carrier' of G1,G)):]

v `1_4 is Element of bool G

v `1 is set

(v `1) `1 is set

((v `1) `1) `1 is set

v `2_4 is Element of bool the carrier' of G1

((v `1) `1) `2 is set

s is Relation-like e -defined y -valued Function-like total quasi_total Element of bool [:e,y:]

v `3_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)

(v `1) `2 is set

t is Relation-like e -defined y -valued Function-like total quasi_total Element of bool [:e,y:]

v `4_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)

x is non empty feasible () ()

(y,e,s,t) is () ()

T2 is non empty feasible () (G1)

the carrier of T2 is non empty set

the carrier' of T2 is set

the of T2 is Relation-like the carrier' of T2 -defined the carrier of T2 -valued Function-like total quasi_total Element of bool [: the carrier' of T2, the carrier of T2:]

[: the carrier' of T2, the carrier of T2:] is Relation-like set

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

the of T2 is Relation-like the carrier' of T2 -defined the carrier of T2 -valued Function-like total quasi_total Element of bool [: the carrier' of T2, the carrier of T2:]

[ the carrier of T2, the carrier' of T2, the of T2, the of T2] is V15() V16() V17() set

[ the carrier of T2, the carrier' of T2, the of T2] is V15() V16() set

[ the carrier of T2, the carrier' of T2] is V15() set

{ the carrier of T2, the carrier' of T2} is non empty finite set

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

{{ the carrier of T2, the carrier' of T2},{ the carrier of T2}} is non empty finite V37() set

[[ the carrier of T2, the carrier' of T2], the of T2] is V15() set

{[ the carrier of T2, the carrier' of T2], the of T2} is non empty finite set

{[ the carrier of T2, the carrier' of T2]} is Relation-like Function-like constant non empty trivial finite 1 -element set

{{[ the carrier of T2, the carrier' of T2], the of T2},{[ the carrier of T2, the carrier' of T2]}} is non empty finite V37() set

[[ the carrier of T2, the carrier' of T2, the of T2], the of T2] is V15() set

{[ the carrier of T2, the carrier' of T2, the of T2], the of T2} is non empty finite set

{[ the carrier of T2, the carrier' of T2, the of T2]} is non empty trivial finite 1 -element set

{{[ the carrier of T2, the carrier' of T2, the of T2], the of T2},{[ the carrier of T2, the carrier' of T2, the of T2]}} is non empty finite V37() set

v is V15() V16() V17() set

y is non empty set

[: the carrier' of T2,y:] is Relation-like set

bool [: the carrier' of T2,y:] is non empty set

x is Element of [:(bool G),(bool the carrier' of G1),(PFuncs ( the carrier' of G1,G)),(PFuncs ( the carrier' of G1,G)):]

x `1_4 is Element of bool G

x `1 is set

(x `1) `1 is set

((x `1) `1) `1 is set

x `2_4 is Element of bool the carrier' of G1

((x `1) `1) `2 is set

s is Relation-like the carrier' of T2 -defined y -valued Function-like total quasi_total Element of bool [: the carrier' of T2,y:]

x `3_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)

(x `1) `2 is set

t is Relation-like the carrier' of T2 -defined y -valued Function-like total quasi_total Element of bool [: the carrier' of T2,y:]

x `4_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)

s is set

e is non empty set

[:s,e:] is Relation-like set

bool [:s,e:] is non empty set

v is set

x is Element of [:(bool G),(bool the carrier' of G1),(PFuncs ( the carrier' of G1,G)),(PFuncs ( the carrier' of G1,G)):]

x `1_4 is Element of bool G

x `1 is set

(x `1) `1 is set

((x `1) `1) `1 is set

x `2_4 is Element of bool the carrier' of G1

((x `1) `1) `2 is set

t is Relation-like s -defined e -valued Function-like total quasi_total Element of bool [:s,e:]

x `3_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)

(x `1) `2 is set

c

x `4_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)

y is non empty feasible () ()

(e,s,t,c

G is set

G2 is set

F

(F

G1 is set

G is set

G1 is non empty feasible ()

the carrier' of G1 is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier of G1 is non empty set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

G is non empty feasible ()

the carrier' of G is set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier of G is non empty 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

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

G1 is non empty feasible ()

the carrier of G1 is non empty set

G is Element of the carrier of G1

G is set

G1 is non empty feasible ()

the carrier' of G1 is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier of G1 is non empty set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 . G is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the of G1 . G is set

G is non empty feasible ()

the carrier' of G is set

G2 is Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like (G)

G1 is ext-real V24() V25() V26() V27() V31() V32() finite cardinal Element of NAT

Seg G1 is finite G1 -element Element of bool NAT

G2 | (Seg G1) is Relation-like NAT -defined Seg G1 -defined NAT -defined the carrier' of G -valued Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier' of G:]

[:NAT, the carrier' of G:] is Relation-like set

bool [:NAT, the carrier' of G:] is non empty set

G1 is non empty feasible ()

the carrier' of G1 is set

the carrier of G1 is non empty set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

G is non empty feasible ()

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier' of G is set

the carrier of G is non empty 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 of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

G2 is set

G is set

v is set

[G,v] is V15() set

{G,v} is non empty finite set

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

{{G,v},{G}} is non empty finite V37() set

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

the of G1 . G is set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

the of G . G is set

G2 is set

G is set

v is set

[G,v] is V15() set

{G,v} is non empty finite set

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

{{G,v},{G}} is non empty finite V37() set

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

the of G1 . G is set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

the of G . G is set

G1 is non empty feasible ()

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier' of G1 is set

the carrier of G1 is non empty set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

G is non empty feasible ()

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier' of G is set

the carrier of G is non empty 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 of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

(G1,G) is non empty feasible () ()

the of (G1,G) is Relation-like the carrier' of (G1,G) -defined the carrier of (G1,G) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,G), the carrier of (G1,G):]

the carrier' of (G1,G) is set

the carrier of (G1,G) is non empty set

[: the carrier' of (G1,G), the carrier of (G1,G):] is Relation-like set

bool [: the carrier' of (G1,G), the carrier of (G1,G):] is non empty set

the of G1 \/ the of G is Relation-like set

the of (G1,G) is Relation-like the carrier' of (G1,G) -defined the carrier of (G1,G) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,G), the carrier of (G1,G):]

the of G1 \/ the of G is Relation-like set

v is set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty finite set

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

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

dom the of (G1,G) is Element of bool the carrier' of (G1,G)

bool the carrier' of (G1,G) is non empty set

the carrier' of G1 \/ the carrier' of G is set

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

the of G1 . x is set

the of (G1,G) . x is set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

the of G . x is set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty finite set

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

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

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

the of G1 . x is set

the carrier' of G1 \/ the carrier' of G is set

dom the of (G1,G) is Element of bool the carrier' of (G1,G)

bool the carrier' of (G1,G) is non empty set

the of (G1,G) . x is set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty finite set

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

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

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

the of G . x is set

the of (G1,G) . x is set

v is set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty finite set

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

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

dom the of (G1,G) is Element of bool the carrier' of (G1,G)

bool the carrier' of (G1,G) is non empty set

the carrier' of G1 \/ the carrier' of G is set

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

the of G1 . x is set

the of (G1,G) . x is set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

the of G . x is set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty finite set

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

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

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

the of G1 . x is set

the carrier' of G1 \/ the carrier' of G is set

dom the of (G1,G) is Element of bool the carrier' of (G1,G)

bool the carrier' of (G1,G) is non empty set

the of (G1,G) . x is set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty finite set

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

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

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

the of G . x is set

the of (G1,G) . x is set

G1 is non empty feasible () ()

(G1,G1) is non empty feasible () ()

the carrier of (G1,G1) is non empty set

the carrier of G1 is non empty set

the carrier of G1 \/ the carrier of G1 is non empty set

the carrier' of (G1,G1) is set

the carrier' of G1 is set

the carrier' of G1 \/ the carrier' of G1 is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

the of (G1,G1) is Relation-like the carrier' of (G1,G1) -defined the carrier of (G1,G1) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,G1), the carrier of (G1,G1):]

[: the carrier' of (G1,G1), the carrier of (G1,G1):] is Relation-like set

bool [: the carrier' of (G1,G1), the carrier of (G1,G1):] is non empty set

dom the of (G1,G1) is Element of bool the carrier' of (G1,G1)

bool the carrier' of (G1,G1) is non empty set

G is set

the of G1 . G is set

the of (G1,G1) . G is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

dom the of G1 is Element of bool the carrier' of G1

the of (G1,G1) is Relation-like the carrier' of (G1,G1) -defined the carrier of (G1,G1) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,G1), the carrier of (G1,G1):]

dom the of (G1,G1) is Element of bool the carrier' of (G1,G1)

G is set

the of G1 . G is set

the of (G1,G1) . G is set

G1 is non empty feasible ()

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier' of G1 is set

the carrier of G1 is non empty set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

G is non empty feasible ()

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier' of G is set

the carrier of G is non empty 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 of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

(G1,G) is non empty feasible () ()

(G,G1) is non empty feasible () ()

the carrier of (G1,G) is non empty set

the carrier of G \/ the carrier of G1 is non empty set

the carrier of (G,G1) is non empty set

the carrier' of (G1,G) is set

the carrier' of G \/ the carrier' of G1 is set

the carrier' of (G,G1) is set

the of (G1,G) is Relation-like the carrier' of (G1,G) -defined the carrier of (G1,G) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,G), the carrier of (G1,G):]

[: the carrier' of (G1,G), the carrier of (G1,G):] is Relation-like set

bool [: the carrier' of (G1,G), the carrier of (G1,G):] is non empty set

dom the of (G1,G) is Element of bool the carrier' of (G1,G)

bool the carrier' of (G1,G) is non empty set

the of (G,G1) is Relation-like the carrier' of (G,G1) -defined the carrier of (G,G1) -valued Function-like total quasi_total Element of bool [: the carrier' of (G,G1), the carrier of (G,G1):]

[: the carrier' of (G,G1), the carrier of (G,G1):] is Relation-like set

bool [: the carrier' of (G,G1), the carrier of (G,G1):] is non empty set

dom the of (G,G1) is Element of bool the carrier' of (G,G1)

bool the carrier' of (G,G1) is non empty set

G2 is set

the of (G1,G) . G2 is set

the of (G,G1) . G2 is set

the carrier' of G1 \/ the carrier' of G is set

the of G1 . G2 is set

the of G . G2 is set

the of (G1,G) is Relation-like the carrier' of (G1,G) -defined the carrier of (G1,G) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,G), the carrier of (G1,G):]

dom the of (G1,G) is Element of bool the carrier' of (G1,G)

the of (G,G1) is Relation-like the carrier' of (G,G1) -defined the carrier of (G,G1) -valued Function-like total quasi_total Element of bool [: the carrier' of (G,G1), the carrier of (G,G1):]

dom the of (G,G1) is Element of bool the carrier' of (G,G1)

G2 is set

the of (G1,G) . G2 is set

the of (G,G1) . G2 is set

the carrier' of G1 \/ the carrier' of G is set

the of G1 . G2 is set

the of G . G2 is set

G1 is non empty feasible ()

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the carrier' of G1 is set

the carrier of G1 is non empty set

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

G is non empty feasible ()

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier' of G is set

the carrier of G is non empty 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 of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

(G1,G) is non empty feasible () ()

G2 is non empty feasible ()

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

the carrier' of G2 is set

the carrier of G2 is non empty set

[: the carrier' of G2, the carrier of G2:] is Relation-like set

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

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

((G1,G),G2) is non empty feasible () ()

(G,G2) is non empty feasible () ()

(G1,(G,G2)) is non empty feasible () ()

the carrier' of (G1,G) is set

the of (G1,G) is Relation-like the carrier' of (G1,G) -defined the carrier of (G1,G) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,G), the carrier of (G1,G):]

the carrier of (G1,G) is non empty set

[: the carrier' of (G1,G), the carrier of (G1,G):] is Relation-like set

bool [: the carrier' of (G1,G), the carrier of (G1,G):] is non empty set

dom the of (G1,G) is Element of bool the carrier' of (G1,G)

bool the carrier' of (G1,G) is non empty set

dom the of G2 is Element of bool the carrier' of G2

bool the carrier' of G2 is non empty set

(dom the of (G1,G)) /\ (dom the of G2) is Element of bool the carrier' of G2

G is set

the of (G1,G) . G is set

the of G2 . G is set

the carrier' of G1 \/ the carrier' of G is set

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

(dom the of G1) /\ (dom the of G2) is Element of bool the carrier' of G2

the of G1 . G is set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

(dom the of G) /\ (dom the of G2) is Element of bool the carrier' of G2

the of G . G is set

the of (G1,G) is Relation-like the carrier' of (G1,G) -defined the carrier of (G1,G) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,G), the carrier of (G1,G):]

dom the of (G1,G) is Element of bool the carrier' of (G1,G)

dom the of G2 is Element of bool the carrier' of G2

(dom the of (G1,G)) /\ (dom the of G2) is Element of bool the carrier' of G2

G is set

the of (G1,G) . G is set

the of G2 . G is set

the carrier' of G1 \/ the carrier' of G is set

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

(dom the of G1) /\ (dom the of G2) is Element of bool the carrier' of G2

the of G1 . G is set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

(dom the of G) /\ (dom the of G2) is Element of bool the carrier' of G2

the of G . G is set

the carrier' of (G,G2) is set

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

the of (G,G2) is Relation-like the carrier' of (G,G2) -defined the carrier of (G,G2) -valued Function-like total quasi_total Element of bool [: the carrier' of (G,G2), the carrier of (G,G2):]

the carrier of (G,G2) is non empty set

[: the carrier' of (G,G2), the carrier of (G,G2):] is Relation-like set

bool [: the carrier' of (G,G2), the carrier of (G,G2):] is non empty set

dom the of (G,G2) is Element of bool the carrier' of (G,G2)

bool the carrier' of (G,G2) is non empty set

(dom the of G1) /\ (dom the of (G,G2)) is Element of bool the carrier' of (G,G2)

G is set

the of G1 . G is set

the of (G,G2) . G is set

the carrier' of G \/ the carrier' of G2 is set

the carrier' of G \/ (dom the of G2) is set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

(dom the of G) \/ (dom the of G2) is set

(dom the of G1) /\ (dom the of G) is Element of bool the carrier' of G

the of G . G is set

(dom the of G1) /\ (dom the of G2) is Element of bool the carrier' of G2

the of G2 . G is set

dom the of G1 is Element of bool the carrier' of G1

the of (G,G2) is Relation-like the carrier' of (G,G2) -defined the carrier of (G,G2) -valued Function-like total quasi_total Element of bool [: the carrier' of (G,G2), the carrier of (G,G2):]

dom the of (G,G2) is Element of bool the carrier' of (G,G2)

(dom the of G1) /\ (dom the of (G,G2)) is Element of bool the carrier' of (G,G2)

G is set

the of G1 . G is set

the of (G,G2) . G is set

the carrier' of G \/ the carrier' of G2 is set

the carrier' of G \/ (dom the of G2) is set

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

(dom the of G) \/ (dom the of G2) is set

(dom the of G1) /\ (dom the of G) is Element of bool the carrier' of G

the of G . G is set

(dom the of G1) /\ (dom the of G2) is Element of bool the carrier' of G2

the of G2 . G is set

the carrier' of ((G1,G),G2) is set

the carrier' of (G1,G) \/ the carrier' of G2 is set

the carrier' of G1 \/ the carrier' of G is set

( the carrier' of G1 \/ the carrier' of G) \/ the carrier' of G2 is set

the carrier' of G \/ the carrier' of G2 is set

the carrier' of G1 \/ ( the carrier' of G \/ the carrier' of G2) is set

the carrier' of G1 \/ the carrier' of (G,G2) is set

the carrier' of (G1,(G,G2)) is set

the carrier of ((G1,G),G2) is non empty set

the carrier of (G1,G) \/ the carrier of G2 is non empty set

the carrier of G1 \/ the carrier of G is non empty set

( the carrier of G1 \/ the carrier of G) \/ the carrier of G2 is non empty set

the carrier of G \/ the carrier of G2 is non empty set

the carrier of G1 \/ ( the carrier of G \/ the carrier of G2) is non empty set

the carrier of G1 \/ the carrier of (G,G2) is non empty set

the carrier of (G1,(G,G2)) is non empty set

the of ((G1,G),G2) is Relation-like the carrier' of ((G1,G),G2) -defined the carrier of ((G1,G),G2) -valued Function-like total quasi_total Element of bool [: the carrier' of ((G1,G),G2), the carrier of ((G1,G),G2):]

[: the carrier' of ((G1,G),G2), the carrier of ((G1,G),G2):] is Relation-like set

bool [: the carrier' of ((G1,G),G2), the carrier of ((G1,G),G2):] is non empty set

dom the of ((G1,G),G2) is Element of bool the carrier' of ((G1,G),G2)

bool the carrier' of ((G1,G),G2) is non empty set

the of (G1,(G,G2)) is Relation-like the carrier' of (G1,(G,G2)) -defined the carrier of (G1,(G,G2)) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,(G,G2)), the carrier of (G1,(G,G2)):]

[: the carrier' of (G1,(G,G2)), the carrier of (G1,(G,G2)):] is Relation-like set

bool [: the carrier' of (G1,(G,G2)), the carrier of (G1,(G,G2)):] is non empty set

dom the of (G1,(G,G2)) is Element of bool the carrier' of (G1,(G,G2))

bool the carrier' of (G1,(G,G2)) is non empty set

G is set

the of ((G1,G),G2) . G is set

the of (G1,(G,G2)) . G is set

the of (G1,G) . G is set

the of G1 . G is set

the of G . G is set

the of (G,G2) . G is set

the of G2 . G is set

the of ((G1,G),G2) is Relation-like the carrier' of ((G1,G),G2) -defined the carrier of ((G1,G),G2) -valued Function-like total quasi_total Element of bool [: the carrier' of ((G1,G),G2), the carrier of ((G1,G),G2):]

dom the of ((G1,G),G2) is Element of bool the carrier' of ((G1,G),G2)

the of (G1,(G,G2)) is Relation-like the carrier' of (G1,(G,G2)) -defined the carrier of (G1,(G,G2)) -valued Function-like total quasi_total Element of bool [: the carrier' of (G1,(G,G2)), the carrier of (G1,(G,G2)):]

dom the of (G1,(G,G2)) is Element of bool the carrier' of (G1,(G,G2))

G is set

the of ((G1,G),G2) . G is set

the of (G1,(G,G2)) . G is set

the of (G1,G) . G is set

the of G1 . G is set

the of G . G is set

the of (G,G2) . G is set

the of G2 . G is set

G1 is non empty feasible ()

G is non empty feasible ()

G2 is non empty feasible ()

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier' of G is set

the carrier of G is non empty 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 of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

the carrier' of G2 is set

the carrier of G2 is non empty set

[: the carrier' of G2, the carrier of G2:] is Relation-like set

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

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

the carrier of G1 is non empty set

the carrier' of G1 is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

( the carrier of G1, the carrier' of G1, the of G1, the of G1) is () ()

(G,G2) is non empty feasible () ()

(G2,G) is non empty feasible () ()

G1 is non empty feasible () ()

(G1,G1) is non empty feasible () ()

G1 is non empty feasible ()

G is non empty feasible ()

(G1,G) is non empty feasible () ()

(G,G1) is non empty feasible () ()

G2 is non empty feasible ()

the carrier' of G1 is set

the carrier of G1 is non empty set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

the carrier' of G2 is set

the carrier of G2 is non empty set

[: the carrier' of G2, the carrier of G2:] is Relation-like set

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

the carrier' of G is set

the carrier of G is non empty set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total 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 of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

G1 is non empty feasible ()

G is non empty feasible ()

(G1,G) is non empty feasible () ()

G2 is non empty feasible ()

((G1,G),G2) is non empty feasible () ()

(G,G2) is non empty feasible () ()

(G1,(G,G2)) is non empty feasible () ()

G is non empty feasible ()

the carrier' of G1 is set

the carrier of G1 is non empty set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the carrier' of G is set

the carrier of G is non empty 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 carrier' of G is set

the carrier of G is non empty set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total 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 G2 is set

the carrier of G2 is non empty set

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

[: the carrier' of G2, the carrier of G2:] is Relation-like set

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

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

G1 is non empty feasible ()

the carrier' of G1 is set

G1 is non empty feasible ()

G is non empty feasible () (G1)

the carrier of G is non empty set

G2 is non empty feasible () (G1)

the carrier of G2 is non empty set

the carrier' of G is set

the carrier' of G2 is set

G1 is non empty feasible () ()

G is non empty feasible () ()

the carrier of G1 is non empty set

the carrier of G is non empty set

the carrier' of G1 is set

the carrier' of G is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

dom the of G1 is Element of bool the carrier' of G1

bool the carrier' of G1 is non empty set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total 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

dom the of G is Element of bool the carrier' of G

bool the carrier' of G is non empty set

G2 is set

the of G1 . G2 is set

the of G . G2 is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

dom the of G1 is Element of bool the carrier' of G1

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

dom the of G is Element of bool the carrier' of G

G2 is set

the of G1 . G2 is set

the of G . G2 is set

G1 is non empty feasible ()

G is non empty feasible ()

G2 is non empty feasible ()

the carrier of G1 is non empty set

the carrier of G is non empty set

the carrier of G2 is non empty set

the carrier' of G1 is set

the carrier' of G is set

the carrier' of G2 is set

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

[: the carrier' of G1, the carrier of G1:] is Relation-like set

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

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

[: the carrier' of G2, the carrier of G2:] is Relation-like set

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

the of G1 is Relation-like the carrier' of G1 -defined the carrier of G1 -valued Function-like total quasi_total Element of bool [: the carrier' of G1, the carrier of G1:]

the of G2 is Relation-like the carrier' of G2 -defined the carrier of G2 -valued Function-like total quasi_total Element of bool [: the carrier' of G2, the carrier of G2:]

G is set

the of G1 . G is set

the of G2 . G is set

the of G1 . G is set

the of G2 . G is set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total 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 of G . G is set

the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier of G:]

the of G . G is set