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

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

(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

(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

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

({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

() + 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

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

G1 is non empty feasible ()

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

() + 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

G1 is non empty feasible ()
the carrier' of G1 is set

rng G is finite set
G2 is set

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

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

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

G2 is set
dom G is finite set
G is set
G . G2 is set
G . G is set

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

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

[:NAT, the carrier' of G:] is Relation-like set
bool [:NAT, the carrier' of G:] is non empty 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 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

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

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) /\ (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 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

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

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
c18 is set
c17 is non empty set
[:c18,c17:] is Relation-like set
bool [:c18,c17:] is non empty set
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

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

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
c15 is Element of [:(bool G),(bool the carrier' of G1),(PFuncs ( the carrier' of G1,G)),(PFuncs ( the carrier' of G1,G)):]
c15 `1_4 is Element of bool G
c15 `1 is set
(c15 `1) `1 is set
((c15 `1) `1) `1 is set
c15 `2_4 is Element of bool the carrier' of G1
((c15 `1) `1) `2 is set
c19 is Relation-like c18 -defined c17 -valued Function-like total quasi_total Element of bool [:c18,c17:]
c15 `3_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)
(c15 `1) `2 is set
c20 is Relation-like c18 -defined c17 -valued Function-like total quasi_total Element of bool [:c18,c17:]
c15 `4_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)
c16 is non empty feasible () ()
(c17,c18,c19,c20) is () ()
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

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

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

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

x `4_4 is Relation-like Function-like Element of PFuncs ( the carrier' of G1,G)
y is non empty feasible () ()
(e,s,t,c15) is () ()
G is set
G2 is set
F1() is non empty feasible ()
(F1()) is set
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

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

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