:: GLIB_001 semantic presentation

REAL is set

NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal Element of K32(REAL)

K32(REAL) is non empty set

COMPLEX is set

NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal set

K32(NAT) is non empty non trivial non finite set

K32(NAT) is non empty non trivial non finite set

{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() set

1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

3 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

_GraphSelectors is non empty Element of K32(NAT)

card {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() set

Seg 1 is non empty trivial finite 1 -element Element of K32(NAT)

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

Seg 2 is non empty finite 2 -element Element of K32(NAT)

{1,2} is non empty finite V49() set

Seg 3 is non empty finite 3 -element Element of K32(NAT)

K5(1,2,3) is non empty finite set

0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() Element of NAT

G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

G2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(G1 + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 - 0 is non empty V28() V29() V30() ext-real positive non negative set

(G1 + 2) - 2 is V28() V29() V30() ext-real set

G1 is set

G2 is Relation-like NAT -defined G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G1

K32(G2) is non empty finite V49() set

len G2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

W1 is Relation-like NAT -defined G1 -valued Function-like finite FinSubsequence-like Element of K32(G2)

Seq W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len (Seq W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

dom W1 is finite Element of K32(NAT)

Sgm (dom W1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(Sgm (dom W1)) * W1 is Relation-like NAT -defined G1 -valued Function-like finite set

dom G2 is finite Element of K32(NAT)

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

rng (Sgm (dom W1)) is finite Element of K32(NAT)

len (Sgm (dom W1)) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

card (dom W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

card W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

G1 is set

G2 is Relation-like NAT -defined G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G1

K32(G2) is non empty finite V49() set

dom G2 is finite Element of K32(NAT)

W1 is Relation-like NAT -defined G1 -valued Function-like finite FinSubsequence-like Element of K32(G2)

Seq W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom (Seq W1) is finite Element of K32(NAT)

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

(Seq W1) . W2 is set

dom W1 is finite Element of K32(NAT)

Sgm (dom W1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(Sgm (dom W1)) . W2 is set

vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

Seg vs is finite vs -element Element of K32(NAT)

(Sgm (dom W1)) * W1 is Relation-like NAT -defined G1 -valued Function-like finite set

dom ((Sgm (dom W1)) * W1) is finite Element of K32(NAT)

W1 . ((Sgm (dom W1)) . W2) is set

[((Sgm (dom W1)) . W2),((Seq W1) . W2)] is V1() set

dom (Sgm (dom W1)) is finite Element of K32(NAT)

G2 . ((Sgm (dom W1)) . W2) is set

G1 is set

G2 is Relation-like NAT -defined G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G1

K32(G2) is non empty finite V49() set

W1 is Relation-like NAT -defined G1 -valued Function-like finite FinSubsequence-like Element of K32(G2)

Seq W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len (Seq W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

card W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

dom W1 is finite Element of K32(NAT)

Sgm (dom W1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

(Sgm (dom W1)) * W1 is Relation-like NAT -defined G1 -valued Function-like finite set

rng (Sgm (dom W1)) is finite Element of K32(NAT)

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

Seg W2 is finite W2 -element Element of K32(NAT)

dom (Seq W1) is finite Element of K32(NAT)

dom (Sgm (dom W1)) is finite Element of K32(NAT)

card (dom W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

Seg (card (dom W1)) is finite card (dom W1) -element Element of K32(NAT)

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

Seg W2 is finite W2 -element Element of K32(NAT)

G1 is set

G2 is Relation-like NAT -defined G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of G1

K32(G2) is non empty finite V49() set

W1 is Relation-like NAT -defined G1 -valued Function-like finite FinSubsequence-like Element of K32(G2)

Seq W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dom (Seq W1) is finite Element of K32(NAT)

dom W1 is finite Element of K32(NAT)

Sgm (dom W1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

dom (Sgm (dom W1)) is finite Element of K32(NAT)

rng (Sgm (dom W1)) is finite Element of K32(NAT)

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

Seg W2 is finite W2 -element Element of K32(NAT)

(Sgm (dom W1)) * W1 is Relation-like NAT -defined G1 -valued Function-like finite set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

choose (the_Vertices_of G1) is Element of the_Vertices_of G1

<*(choose (the_Vertices_of G1))*> is non empty trivial Relation-like NAT -defined the_Vertices_of G1 -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1

W2 is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1

len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

W2 . y is set

y + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

W2 . (y + 1) is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Edges_of G1 is set

the_Vertices_of G1 is non empty set

<*> (the_Edges_of G1) is empty Relation-like non-empty empty-yielding NAT -defined the_Edges_of G1 -valued Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() FinSequence of the_Edges_of G1

choose (the_Vertices_of G1) is Element of the_Vertices_of G1

<*(choose (the_Vertices_of G1))*> is non empty trivial Relation-like NAT -defined the_Vertices_of G1 -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1

len (<*> (the_Edges_of G1)) is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() Element of NAT

(len (<*> (the_Edges_of G1))) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

W2 is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1

len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

W2 . y is set

y + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

W2 . (y + 1) is set

(<*> (the_Edges_of G1)) . y is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

W1 is set

W2 is Element of (the_Vertices_of G1) \/ (the_Edges_of G1)

<*W2*> is non empty trivial Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

len <*W2*> is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

<*W2*> . 1 is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

<*W2*> . y is set

y + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

<*W2*> . (y + 2) is set

y + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

<*W2*> . (y + 1) is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

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

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

vs is Element of (the_Vertices_of G1) \/ (the_Edges_of G1)

<*vs*> is non empty trivial Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

vs is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

vs . 1 is set

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

len <*G2*> is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

vs . vs is set

vs + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

vs . (vs + 2) is set

vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

vs . (vs + 1) is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

G2 is set

W1 is set

W2 is set

<*G2,W2,W1*> is non empty Relation-like NAT -defined Function-like finite 3 -element FinSequence-like FinSubsequence-like set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

choose (the_Vertices_of G1) is Element of the_Vertices_of G1

(G1,(choose (the_Vertices_of G1))) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

<*(choose (the_Vertices_of G1))*> is non empty trivial Relation-like NAT -defined the_Vertices_of G1 -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1

vs is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

vs . 1 is set

vs . 2 is set

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

vs + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

2 * 1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

2 * 0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V86() even Element of NAT

vs . n is set

n + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

vs . (n + 2) is set

n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

vs . (n + 1) is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

G2 . 1 is set

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (len G2) is set

(len G2) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

2 * 1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(len G2) - (2 * 1) is non empty V28() V29() V30() ext-real non even set

W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W1 is set

W1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

G2 . (W1 + 1) is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W1 is set

(G1,G2) is Element of the_Vertices_of G1

G2 . 1 is set

(G1,G2) is Element of the_Vertices_of G1

G2 . (len G2) is set

W1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

G2 . (W1 + 2) is set

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

G2 . (W2 + 1) is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

Rev G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

W2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W2 . 1 is set

(G1,G2) is Element of the_Vertices_of G1

G2 . (len G2) is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(len G2) - y is V28() V29() V30() ext-real even set

((len G2) - y) + 1 is non empty V28() V29() V30() ext-real non even set

y + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(len G2) - (y + 1) is non empty V28() V29() V30() ext-real non even set

((len G2) - (y + 1)) + 1 is V28() V29() V30() ext-real even set

y + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(len G2) - (y + 2) is V28() V29() V30() ext-real even set

((len G2) - (y + 2)) + 1 is non empty V28() V29() V30() ext-real non even set

(y + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

dom G2 is finite Element of K32(NAT)

W2 . (y + 1) is set

n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

G2 . n is set

n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

G2 . (n + 1) is set

W2 . y is set

x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . x is set

n + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (n + 2) is set

1 + 0 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

(len G2) - 1 is V28() V29() V30() ext-real even set

((len G2) - 1) + 1 is non empty V28() V29() V30() ext-real non even set

G2 . n is set

W2 . (y + 2) is set

W1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

W2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

Rev W2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

Rev W1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,G2) is Element of the_Vertices_of G1

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (len G2) is set

W1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,W1) is Element of the_Vertices_of G1

W1 . 1 is set

G2 ^' W1 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

len (G2 ^' W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(G2 ^' W1) . vs is set

vs + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(G2 ^' W1) . (vs + 2) is set

vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(G2 ^' W1) . (vs + 1) is set

(vs + 2) - 2 is V28() V29() V30() ext-real set

(len G2) - 0 is non empty V28() V29() V30() ext-real positive non negative set

G2 . vs is set

(vs + 2) - 1 is V28() V29() V30() ext-real even set

G2 . (vs + 1) is set

G2 . (vs + 2) is set

(len G2) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(vs + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

(len G2) + n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

x is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

x + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

0 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

(len (G2 ^' W1)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

len W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(len G2) + (len W1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

((len G2) + (len W1)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(len W1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(len G2) + ((len W1) + 1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

x + (len G2) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W1 . (x + 1) is set

1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

(1 + 1) + 0 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

W1 . (1 + 1) is set

2 * 1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

xaa1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

x - xaa1 is V28() V29() V30() ext-real even set

(x + (len G2)) - (len G2) is V28() V29() V30() ext-real even set

2 + (len G2) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(2 + (len G2)) - (len G2) is V28() V29() V30() ext-real even set

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(W2 + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

((W2 + 1) + 1) - 1 is non empty V28() V29() V30() ext-real non even set

1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

(1 + 1) - 1 is V28() V29() V30() ext-real set

(len W1) - 0 is non empty V28() V29() V30() ext-real positive non negative set

es is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

es + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(es + 1) - 1 is non empty V28() V29() V30() ext-real non even set

W1 . (es + 1) is set

(len G2) + es is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(G2 ^' W1) . ((len G2) + es) is set

es + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W1 . (es + 2) is set

W2 + (1 + 1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

(len G2) + W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

((len G2) + W2) + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W1 . (W2 + 1) is set

vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

len W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(len G2) + (len W1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(G2 ^' W1) . 1 is set

(G1,G2) is Element of the_Vertices_of G1

G2 . 1 is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(W1,W2) -cut G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1)

len ((W1,W2) -cut G2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even set

(len ((W1,W2) -cut G2)) + vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

((len ((W1,W2) -cut G2)) + vs) - vs is V28() V29() V30() ext-real set

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even set

vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(vs + 1) - vs is non empty V28() V29() V30() ext-real non even set

n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

n - 1 is V28() V29() V30() ext-real even set

n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

0 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

((W1,W2) -cut G2) . (0 + 1) is set

W1 + 0 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

G2 . (W1 + 0) is set

G2 . W1 is set

(G1,G2,W1) is Element of the_Vertices_of G1

((W1,W2) -cut G2) . 1 is set

x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

vs + x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(vs + x) - 1 is non empty V28() V29() V30() ext-real non even set

x - 1 is V28() V29() V30() ext-real even set

x + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

(x + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

((W1,W2) -cut G2) . ((x + 1) + 1) is set

W1 + (x + 1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

G2 . (W1 + (x + 1)) is set

(len ((W1,W2) -cut G2)) + W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

x + W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

x + vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

W1 + x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

(len G2) - 0 is non empty V28() V29() V30() ext-real positive non negative set

(W1 + x) - 1 is V28() V29() V30() ext-real set

xaa1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . xaa1 is set

xaa1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (xaa1 + 2) is set

xaa1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

G2 . (xaa1 + 1) is set

(len ((W1,W2) -cut G2)) - 0 is V28() V29() V30() ext-real non negative set

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

((W1,W2) -cut G2) . (W2 + 1) is set

W1 + W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

G2 . (W1 + W2) is set

((W1,W2) -cut G2) . x is set

x + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

((W1,W2) -cut G2) . (x + 2) is set

((W1,W2) -cut G2) . (x + 1) is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W1 is set

G2 . W2 is set

(G1,G2,1,W1) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,G2,W2,(len G2)) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,(G1,G2,1,W1),(G1,G2,W2,(len G2))) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,G2) is Element of the_Vertices_of G1

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (len G2) is set

W1 is set

(G1,G2) .adj W1 is Element of the_Vertices_of G1

(G1,(G1,G2),((G1,G2) .adj W1),W1) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,G2,(G1,(G1,G2),((G1,G2) .adj W1),W1)) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(len G2) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

W1 div 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

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

len y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

dom y is finite Element of K32(NAT)

2 * (W1 div 2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

vs is set

rng y is finite set

vs is set

y . vs is set

Seg (W1 div 2) is finite W1 div 2 -element Element of K32(NAT)

vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

vs * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

n - 1 is non empty V28() V29() V30() ext-real non even set

1 * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(W1 div 2) * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

xaa1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W1 - 1 is non empty V28() V29() V30() ext-real non even set

G2 . xaa1 is set

(G1,G2,xaa1) is Element of the_Vertices_of G1

vs is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the_Vertices_of G1

vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

vs + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

vs . (vs + 1) is set

len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

n - 1 is non empty V28() V29() V30() ext-real non even set

vs * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

((len G2) + 1) - 1 is non empty V28() V29() V30() ext-real non even set

xaa1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . xaa1 is set

xaa1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (xaa1 + 2) is set

xaa1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

G2 . (xaa1 + 1) is set

dom vs is finite Element of K32(NAT)

2 * (vs + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(2 * (vs + 1)) - 1 is non empty V28() V29() V30() ext-real non even set

G2 . ((2 * (vs + 1)) - 1) is set

n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (n + 1) is set

vs . vs is set

vs is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * (len vs) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

vs . vs is set

2 * vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(2 * vs) - 1 is non empty V28() V29() V30() ext-real non even set

G2 . ((2 * vs) - 1) is set

dom vs is finite Element of K32(NAT)

W1 is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * (len W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

W2 is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * (len W2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

dom W1 is finite Element of K32(NAT)

W1 . y is set

2 * y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(2 * y) - 1 is non empty V28() V29() V30() ext-real non even set

G2 . ((2 * y) - 1) is set

W2 . y is set

Seg (len W2) is finite len W2 -element Element of K32(NAT)

dom W2 is finite Element of K32(NAT)

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(len G2) - 1 is V28() V29() V30() ext-real even set

W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

W1 div 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

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

len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

dom vs is finite Element of K32(NAT)

vs is set

rng vs is finite set

vs is set

vs . vs is set

Seg y is finite y -element Element of K32(NAT)

n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

n * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

y * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

1 * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

n - 1 is non empty V28() V29() V30() ext-real non even set

x is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . x is set

x + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (x + 2) is set

x + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

G2 . (x + 1) is set

G2 . (2 * n) is set

2 * y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(2 * y) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(G1,G2) is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

vs is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the_Edges_of G1

len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * (len vs) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(2 * (len vs)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

((2 * (len vs)) + 1) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

n is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * (len n) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(len vs) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

2 * ((len vs) + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

n . n is set

n + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

n . (n + 1) is set

2 * n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

g is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

g - 1 is non empty V28() V29() V30() ext-real non even set

n + n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

n * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(len vs) * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(len G2) - 0 is non empty V28() V29() V30() ext-real positive non negative set

es is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

2 * (n + 1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(2 * (n + 1)) - 1 is non empty V28() V29() V30() ext-real non even set

G2 . ((2 * (n + 1)) - 1) is set

es + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (es + 2) is set

dom vs is finite Element of K32(NAT)

vs . n is set

es + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

G2 . (es + 1) is set

(2 * n) - 1 is non empty V28() V29() V30() ext-real non even set

G2 . ((2 * n) - 1) is set

n is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

vs is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * (len vs) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(2 * (len vs)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

vs . n is set

2 * n is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

G2 . (2 * n) is set

dom vs is finite Element of K32(NAT)

W1 is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * (len W1) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(2 * (len W1)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W2 is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

2 * (len W2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(2 * (len W2)) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

dom W1 is finite Element of K32(NAT)

W1 . y is set

2 * y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

G2 . (2 * y) is set

W2 . y is set

Seg (len W2) is finite len W2 -element Element of K32(NAT)

dom W2 is finite Element of K32(NAT)

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,G2) is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

rng (G1,G2) is finite Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,G2) is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

rng (G1,G2) is finite Element of K32((the_Edges_of G1))

K32((the_Edges_of G1)) is non empty set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,G2) is Relation-like NAT -defined the_Edges_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len (G1,G2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

W1 is set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,G2) is finite Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty set

(G1,G2) is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

rng (G1,G2) is finite Element of K32((the_Vertices_of G1))

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

dom (G1,G2) is finite Element of K32(NAT)

y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

(G1,G2) . y is set

2 * y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

vs is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even set

vs - 1 is non empty V28() V29() V30() ext-real non even set

y + y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

len (G1,G2) is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

y * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(len (G1,G2)) * 2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

(len G2) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

((len G2) + 1) - 1 is non empty V28() V29() V30() ext-real non even set

n is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . n is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . y is set

y is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

G2 . y is set

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . vs is set

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even set

G2 . vs is set

W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W2 is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . y is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W1 is set

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

G2 . W2 is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . vs is set

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even set

G2 . vs is set

W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W2 is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . y is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

W1 is set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

(G1,G2) is finite Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty set

(G1,G2) is Relation-like NAT -defined the_Vertices_of G1 -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

rng (G1,G2) is finite Element of K32((the_Vertices_of G1))

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(G1,G2,W1) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (G1,G2,W1) is set

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

G2 . W2 is set

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

G2 . W2 is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . vs is set

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . vs is set

W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W2 is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . y is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal Element of NAT

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W1 is set

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

G2 . W2 is set

W2 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal set

G2 . W2 is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . vs is set

vs is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . vs is set

W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W2 is set

y is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . y is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W1 is set

(G1,G2,W1) is Element of the_Vertices_of G1

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

dom G2 is finite Element of K32(NAT)

W1 is V21() V22() V23() V27() V28() V29() V30() ext-real non negative finite cardinal even Element of NAT

W1 - 1 is non empty V28() V29() V30() ext-real non even set

W1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (W1 + 1) is set

G2 . W1 is set

1 + W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . W2 is set

1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal Element of NAT

(1 + 1) - 1 is V28() V29() V30() ext-real set

(len G2) - 0 is non empty V28() V29() V30() ext-real positive non negative set

W2 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G2 . (W2 + 2) is set

W2 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

G2 . (W2 + 1) is set

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

G2 is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

len G2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

dom G2 is finite Element of K32(NAT)

W1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

W1 + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal even Element of NAT

W1 + 2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

G1 is Relation-like NAT -defined Function-like finite [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

(G1,G2) is Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like finite FinSequence-like FinSubsequence-like (G1)

the_Edges_of G1 is set

(the_Vertices_of G1) \/ (the_Edges_of G1) is non empty set

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

(G1,(G1,G2)) is Element of the_Vertices_of G1

(G1,G2) . 1 is set

(G1,(G1,G2)) is Element of the_Vertices_of G1

len (G1,G2) is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(G1,G2) . (len (G1,G2)) is set

W2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative finite cardinal non even Element of NAT

(G1,G2) . W2 is set

the_Source_of G1 is Relation-like Function-like V18( the_Edges_of G1, the_Vertices_of G1) Element of