:: GLIB_002 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V31() cardinal limit_cardinal Element of K32(REAL)

K32(REAL) is non empty set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V31() cardinal limit_cardinal set

K32(NAT) is non empty non trivial non empty-membered V31() set

K32(NAT) is non empty non trivial non empty-membered V31() set

COMPLEX is set

RAT is set

INT is set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() V35() cardinal {} -element V46() V47() Function-yielding V81() V95() ext-real set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real positive Element of NAT

_GraphSelectors is non empty Element of K32(NAT)

card {} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() V35() cardinal {} -element V46() V47() Function-yielding V81() V95() ext-real set

3 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real positive Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real positive Element of NAT

0 is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() V32() V35() cardinal {} -element V46() V47() Function-yielding V81() V95() ext-real Element of NAT

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

{G2} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

G1 .walkOf G2 is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of G1

y is Element of the_Vertices_of G1

y9 is Element of the_Vertices_of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G2 is Relation-like Function-like FinSequence-like Walk of G1

G2 .edges() is V31() Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

x is set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] trivial () set

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Edges_of G1 is set

the_Source_of G1 is Relation-like Function-like V27( the_Edges_of G1) V28( the_Edges_of G1, the_Vertices_of G1) Element of K32(K33((the_Edges_of G1),(the_Vertices_of G1)))

the_Vertices_of G1 is non empty set

K33((the_Edges_of G1),(the_Vertices_of G1)) is Relation-like set

K32(K33((the_Edges_of G1),(the_Vertices_of G1))) is non empty set

the_Target_of G1 is Relation-like Function-like V27( the_Edges_of G1) V28( the_Edges_of G1, the_Vertices_of G1) Element of K32(K33((the_Edges_of G1),(the_Vertices_of G1)))

G2 is set

(the_Source_of G1) . G2 is set

(the_Target_of G1) . G2 is set

y is Element of the_Vertices_of G1

G1 .walkOf (y,G2,y) is Relation-like Function-like FinSequence-like closed Trail-like Path-like Walk of G1

len (G1 .walkOf (y,G2,y)) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

y is set

y9 is set

G2 is set

x is set

G1 .walkOf (y,G2,y9) is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1

(G1 .walkOf (y,G2,y9)) .addEdge x is Relation-like Function-like FinSequence-like Walk of G1

W9 is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1

W9 .last() is Element of the_Vertices_of G1

((G1 .walkOf (y,G2,y9)) .addEdge x) .last() is Element of the_Vertices_of G1

len W9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

W is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

1 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

2 * 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

(2 * 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

<*y,G2,y9*> is set

W9 . W is set

W9 .first() is Element of the_Vertices_of G1

((G1 .walkOf (y,G2,y9)) .addEdge x) .first() is Element of the_Vertices_of G1

W9 .edges() is V31() Element of K32((the_Edges_of G1))

K32((the_Edges_of G1)) is non empty set

{G2} is non empty trivial V31() 1 -element set

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

{G2} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

x is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless trivial non-multi non-Dmulti simple Dsimple () () () inducedSubgraph of G1,{G2}, {}

{1} is non empty trivial V31() V35() 1 -element Element of K32(NAT)

K33({},{1}) is Relation-like V31() set

K32(K33({},{1})) is non empty V31() V35() set

x is Relation-like Function-like V27( {} ) V28( {} ,{1}) V31() Element of K32(K33({},{1}))

createGraph ({1},{},x,x) is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless trivial non-multi non-Dmulti simple Dsimple () () () set

{0,1} is non empty V31() V35() Element of K32(NAT)

{0} is non empty trivial functional V31() V35() 1 -element Element of K32(NAT)

0 .--> 0 is Relation-like NAT -defined {0} -defined NAT -valued Function-like one-to-one V31() Function-yielding V81() set

{0} is non empty trivial functional V31() V35() 1 -element set

{0} --> 0 is non empty Relation-like {0} -defined NAT -valued Function-like constant V27({0}) V28({0},{0}) V31() Function-yielding V81() Element of K32(K33({0},{0}))

K33({0},{0}) is non empty Relation-like V31() set

K32(K33({0},{0})) is non empty non empty-membered V31() V35() set

0 .--> 1 is Relation-like NAT -defined {0} -defined NAT -valued Function-like one-to-one V31() set

{0} --> 1 is non empty Relation-like non-empty {0} -defined NAT -valued Function-like constant V27({0}) V28({0},{1}) V31() Element of K32(K33({0},{1}))

{1} is non empty trivial V31() V35() 1 -element set

K33({0},{1}) is non empty Relation-like V31() set

K32(K33({0},{1})) is non empty non empty-membered V31() V35() set

dom (0 .--> 1) is V31() set

y9 is set

(0 .--> 1) . y9 is set

y9 is set

(0 .--> 0) . y9 is Relation-like Function-like set

K33({0},{0,1}) is non empty Relation-like V31() set

K32(K33({0},{0,1})) is non empty non empty-membered V31() V35() set

dom (0 .--> 0) is V31() set

W is non empty Relation-like Function-like V27({0}) V28({0},{0,1}) V31() Element of K32(K33({0},{0,1}))

y9 is non empty Relation-like Function-like V27({0}) V28({0},{0,1}) V31() Element of K32(K33({0},{0,1}))

createGraph ({0,1},{0},W,y9) is Relation-like NAT -defined Function-like V31() [Graph-like] finite set

the_Edges_of (createGraph ({0,1},{0},W,y9)) is V31() set

the_Vertices_of (createGraph ({0,1},{0},W,y9)) is non empty V31() set

the_Target_of (createGraph ({0,1},{0},W,y9)) is Relation-like Function-like V27( the_Edges_of (createGraph ({0,1},{0},W,y9))) V28( the_Edges_of (createGraph ({0,1},{0},W,y9)), the_Vertices_of (createGraph ({0,1},{0},W,y9))) V31() Element of K32(K33((the_Edges_of (createGraph ({0,1},{0},W,y9))),(the_Vertices_of (createGraph ({0,1},{0},W,y9)))))

K33((the_Edges_of (createGraph ({0,1},{0},W,y9))),(the_Vertices_of (createGraph ({0,1},{0},W,y9)))) is Relation-like V31() set

K32(K33((the_Edges_of (createGraph ({0,1},{0},W,y9))),(the_Vertices_of (createGraph ({0,1},{0},W,y9))))) is non empty V31() V35() set

(the_Target_of (createGraph ({0,1},{0},W,y9))) . 0 is set

the_Source_of (createGraph ({0,1},{0},W,y9)) is Relation-like Function-like V27( the_Edges_of (createGraph ({0,1},{0},W,y9))) V28( the_Edges_of (createGraph ({0,1},{0},W,y9)), the_Vertices_of (createGraph ({0,1},{0},W,y9))) V31() Element of K32(K33((the_Edges_of (createGraph ({0,1},{0},W,y9))),(the_Vertices_of (createGraph ({0,1},{0},W,y9)))))

(the_Source_of (createGraph ({0,1},{0},W,y9))) . 0 is set

W9 is Relation-like Function-like FinSequence-like Walk of createGraph ({0,1},{0},W,y9)

len W9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

1 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

W9 . (1 + 1) is set

W9 . 1 is set

1 + 2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

W9 . (1 + 2) is set

(the_Source_of (createGraph ({0,1},{0},W,y9))) . (W9 . (1 + 1)) is set

(the_Target_of (createGraph ({0,1},{0},W,y9))) . (W9 . (1 + 1)) is set

len W9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

3 - 1 is V46() V47() V95() ext-real set

(len W9) - 0 is V46() V47() V95() ext-real set

2 * 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

dom W9 is Element of K32(NAT)

W9 . (2 * 1) is set

3 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

2 * 2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

W9 . (2 * 2) is set

len W9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

(createGraph ({0,1},{0},W,y9)) .walkOf (0,0,1) is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of createGraph ({0,1},{0},W,y9)

((createGraph ({0,1},{0},W,y9)) .walkOf (0,0,1)) .reverse() is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of createGraph ({0,1},{0},W,y9)

card (the_Vertices_of (createGraph ({0,1},{0},W,y9))) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

v9 is set

{v9} is non empty trivial V31() 1 -element set

v9 is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

C is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

v is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

(createGraph ({0,1},{0},W,y9)) .walkOf v is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of createGraph ({0,1},{0},W,y9)

v9 is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

C is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

v9 is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

C is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

v9 is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

C is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

u9 is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

(createGraph ({0,1},{0},W,y9)) .walkOf u9 is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of createGraph ({0,1},{0},W,y9)

v9 is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

C is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

v9 is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

C is Element of the_Vertices_of (createGraph ({0,1},{0},W,y9))

P is Relation-like Function-like FinSequence-like Walk of createGraph ({0,1},{0},W,y9)

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless trivial non-multi non-Dmulti simple Dsimple () () () Subgraph of G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless trivial non-multi non-Dmulti simple Dsimple () () () Subgraph of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] loopless non-multi non-Dmulti simple Dsimple () set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] loopless non-multi non-Dmulti simple Dsimple Subgraph of G1

x is Relation-like Function-like FinSequence-like Walk of G2

y is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

G2 is Element of the_Vertices_of G1

x is Element of K32((the_Vertices_of G1))

G1 .walkOf G2 is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of G1

y is non empty Element of K32((the_Vertices_of G1))

y9 is set

W is Relation-like Function-like FinSequence-like Walk of G1

W is Relation-like Function-like FinSequence-like Walk of G1

x is non empty Element of K32((the_Vertices_of G1))

y is non empty Element of K32((the_Vertices_of G1))

y9 is set

W is Relation-like Function-like FinSequence-like Walk of G1

W is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

G2 is Element of the_Vertices_of G1

G1 .walkOf G2 is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of G1

y is Element of K32((the_Vertices_of G1))

y9 is non empty Element of K32((the_Vertices_of G1))

W is set

W9 is Relation-like Function-like FinSequence-like directed Walk of G1

x is non empty Element of K32((the_Vertices_of G1))

y is non empty Element of K32((the_Vertices_of G1))

y9 is set

W is Relation-like Function-like FinSequence-like directed Walk of G1

W is Relation-like Function-like FinSequence-like directed Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

(G1,G2) is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

G1 .walkOf G2 is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

(G1,G2) is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

y is set

y9 is set

x is set

W9 is Relation-like Function-like FinSequence-like Walk of G1

W9 .addEdge x is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

x is Element of the_Vertices_of G1

(G1,x) is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

(G1,G2) is non empty Element of K32((the_Vertices_of G1))

y is Relation-like Function-like FinSequence-like Walk of G1

y .reverse() is Relation-like Function-like FinSequence-like Walk of G1

y9 is set

W is Relation-like Function-like FinSequence-like Walk of G1

y .append W is Relation-like Function-like FinSequence-like Walk of G1

W is Relation-like Function-like FinSequence-like Walk of G1

(y .reverse()) .append W is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Relation-like Function-like FinSequence-like Walk of G1

G2 .vertices() is V31() Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

x is Element of the_Vertices_of G1

(G1,x) is non empty Element of K32((the_Vertices_of G1))

len G2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

y is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

G2 . y is set

y9 is set

W is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

G2 . W is set

G2 .cut (y,W) is Relation-like Function-like FinSequence-like Walk of G1

G2 .cut (W,y) is Relation-like Function-like FinSequence-like Walk of G1

(G2 .cut (W,y)) .reverse() is Relation-like Function-like FinSequence-like Walk of G1

W9 is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] Subgraph of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

(G1,G2) is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

G1 .edgesBetween (G1,G2) is Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

x is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(G1,G2),G1 .edgesBetween (G1,G2)

the_Vertices_of x is non empty Element of K32((the_Vertices_of G1))

the_Edges_of x is Element of K32((the_Edges_of G1))

y is Relation-like NAT -defined Function-like V31() [Graph-like] () Subgraph of G1

the_Vertices_of y is non empty Element of K32((the_Vertices_of G1))

y9 is set

W is Relation-like Function-like FinSequence-like Walk of y

W9 is Relation-like Function-like FinSequence-like Walk of G1

y9 is set

the_Edges_of y is Element of K32((the_Edges_of G1))

y9 is set

y9 is set

the_Source_of y is Relation-like Function-like V27( the_Edges_of y) V28( the_Edges_of y, the_Vertices_of y) Element of K32(K33((the_Edges_of y),(the_Vertices_of y)))

the_Edges_of y is set

the_Vertices_of y is non empty set

K33((the_Edges_of y),(the_Vertices_of y)) is Relation-like set

K32(K33((the_Edges_of y),(the_Vertices_of y))) is non empty set

(the_Source_of y) . y9 is set

the_Target_of y is Relation-like Function-like V27( the_Edges_of y) V28( the_Edges_of y, the_Vertices_of y) Element of K32(K33((the_Edges_of y),(the_Vertices_of y)))

(the_Target_of y) . y9 is set

the_Vertices_of x is non empty set

W9 is Element of the_Vertices_of x

W is Element of the_Vertices_of x

the_Edges_of y is Element of K32((the_Edges_of G1))

the_Vertices_of x is non empty set

y is Element of the_Vertices_of x

W is Relation-like Function-like FinSequence-like Walk of G1

y9 is Element of the_Vertices_of x

W9 is Relation-like Function-like FinSequence-like Walk of G1

W .reverse() is Relation-like Function-like FinSequence-like Walk of G1

(W .reverse()) .append W9 is Relation-like Function-like FinSequence-like Walk of G1

(W .reverse()) .last() is Element of the_Vertices_of G1

(W .reverse()) .vertices() is V31() Element of K32((the_Vertices_of G1))

((W .reverse()) .append W9) .edges() is V31() Element of K32((the_Edges_of G1))

((W .reverse()) .append W9) .vertices() is V31() Element of K32((the_Vertices_of G1))

G1 .edgesBetween (((W .reverse()) .append W9) .vertices()) is Element of K32((the_Edges_of G1))

W9 .first() is Element of the_Vertices_of G1

W9 .vertices() is V31() Element of K32((the_Vertices_of G1))

((W .reverse()) .vertices()) \/ (W9 .vertices()) is V31() Element of K32((the_Vertices_of G1))

G1 .edgesBetween (the_Vertices_of x) is Element of K32((the_Edges_of G1))

v is Relation-like Function-like FinSequence-like Walk of x

u9 is Relation-like Function-like FinSequence-like Walk of x

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

the Element of the_Vertices_of G1 is Element of the_Vertices_of G1

(G1, the Element of the_Vertices_of G1) is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

G1 .edgesBetween (G1, the Element of the_Vertices_of G1) is Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

the Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) inducedSubgraph of G1,(G1, the Element of the_Vertices_of G1),G1 .edgesBetween (G1, the Element of the_Vertices_of G1) is Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) inducedSubgraph of G1,(G1, the Element of the_Vertices_of G1),G1 .edgesBetween (G1, the Element of the_Vertices_of G1)

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

K32(K32((the_Vertices_of G1))) is non empty non empty-membered set

the Element of the_Vertices_of G1 is Element of the_Vertices_of G1

bool (the_Vertices_of G1) is non empty non empty-membered Element of K32(K32((the_Vertices_of G1)))

x is Element of K32(K32((the_Vertices_of G1)))

(G1, the Element of the_Vertices_of G1) is non empty Element of K32((the_Vertices_of G1))

y9 is non empty Element of K32(K32((the_Vertices_of G1)))

W is set

W9 is set

W9 is Element of the_Vertices_of G1

(G1,W9) is non empty Element of K32((the_Vertices_of G1))

G2 is non empty Element of K32(K32((the_Vertices_of G1)))

x is non empty Element of K32(K32((the_Vertices_of G1)))

y is set

y9 is Element of the_Vertices_of G1

(G1,y9) is non empty Element of K32((the_Vertices_of G1))

y9 is Element of the_Vertices_of G1

(G1,y9) is non empty Element of K32((the_Vertices_of G1))

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

(G1) is non empty Element of K32(K32((the_Vertices_of G1)))

K32(K32((the_Vertices_of G1))) is non empty non empty-membered set

G2 is Element of (G1)

G1 .edgesBetween G2 is Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

x is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,G2,G1 .edgesBetween G2

y is Element of the_Vertices_of G1

(G1,y) is non empty Element of K32((the_Vertices_of G1))

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

(G1) is non empty Element of K32(K32((the_Vertices_of G1)))

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

K32(K32((the_Vertices_of G1))) is non empty non empty-membered set

card (G1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

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

(G1) is epsilon-transitive epsilon-connected ordinal cardinal set

(G1) is non empty V31() V35() Element of K32(K32((the_Vertices_of G1)))

the_Vertices_of G1 is non empty V31() set

K32((the_Vertices_of G1)) is non empty non empty-membered V31() V35() set

K32(K32((the_Vertices_of G1))) is non empty non empty-membered V31() V35() set

card (G1) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set

card (G1) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

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

the_Vertices_of G1 is non empty V31() set

G2 is Element of the_Vertices_of G1

{G2} is non empty trivial V31() 1 -element set

(the_Vertices_of G1) \ {G2} is V31() Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered V31() V35() set

G1 .edgesBetween ((the_Vertices_of G1) \ {G2}) is V31() Element of K32((the_Edges_of G1))

the_Edges_of G1 is V31() set

K32((the_Edges_of G1)) is non empty V31() V35() set

(G1) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

(G1) is non empty V31() V35() Element of K32(K32((the_Vertices_of G1)))

K32(K32((the_Vertices_of G1))) is non empty non empty-membered V31() V35() set

card (G1) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set

card (G1) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

x is Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})

(x) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

(x) is non empty V31() V35() Element of K32(K32((the_Vertices_of x)))

the_Vertices_of x is non empty V31() set

K32((the_Vertices_of x)) is non empty non empty-membered V31() V35() set

K32(K32((the_Vertices_of x))) is non empty non empty-membered V31() V35() set

card (x) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set

card (x) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

x is Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})

(x) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

(x) is non empty V31() V35() Element of K32(K32((the_Vertices_of x)))

the_Vertices_of x is non empty V31() set

K32((the_Vertices_of x)) is non empty non empty-membered V31() V35() set

K32(K32((the_Vertices_of x))) is non empty non empty-membered V31() V35() set

card (x) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set

card (x) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] non trivial () set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

{G2} is non empty trivial V31() 1 -element set

(the_Vertices_of G1) \ {G2} is Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

G1 .edgesBetween ((the_Vertices_of G1) \ {G2}) is Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

x is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})

the_Vertices_of x is non empty Element of K32((the_Vertices_of G1))

G2 .edgesInOut() is Element of K32((the_Edges_of G1))

W is set

{W} is non empty trivial V31() 1 -element set

the_Vertices_of x is non empty set

W9 is Element of the_Vertices_of x

W9 is Element of the_Vertices_of x

W is Element of the_Vertices_of G1

v is Element of the_Vertices_of G1

u9 is Relation-like Function-like FinSequence-like Walk of G1

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 is Relation-like Function-like FinSequence-like Trail-like Subwalk of u9

len the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 . (len the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9) is set

{G2} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of G1))

(the_Vertices_of G1) \ {G2} is Element of K32((the_Vertices_of G1))

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 . 1 is set

C is set

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 .edges() is V31() Element of K32((the_Edges_of G1))

P is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 . P is set

dom the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 is Element of K32(NAT)

P - 1 is non empty V46() V47() non even V95() ext-real set

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 . (P + 1) is set

P is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 . P is set

P - 1 is V46() V47() even V95() ext-real set

1 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

(1 + 1) - 1 is V46() V47() V95() ext-real set

P is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 .vertexAt P is Element of the_Vertices_of G1

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 . P is set

P - 0 is V46() V47() V95() ext-real set

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 .vertexAt (P + 1) is Element of the_Vertices_of G1

(P + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 . ((P + 1) + 1) is set

1 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

P + (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

P + 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

(the_Edges_of G1) \ (G2 .edgesInOut()) is Element of K32((the_Edges_of G1))

G1 .edgesInOut {G2} is Element of K32((the_Edges_of G1))

(the_Edges_of G1) \ (G1 .edgesInOut {G2}) is Element of K32((the_Edges_of G1))

G1 .edgesBetween ((the_Vertices_of G1) \ {G2}) is Element of K32((the_Edges_of G1))

the_Edges_of x is Element of K32((the_Edges_of G1))

C is set

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 .vertices() is V31() Element of K32((the_Vertices_of G1))

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 .first() is Element of the_Vertices_of G1

the Relation-like Function-like FinSequence-like Trail-like Subwalk of u9 .last() is Element of the_Vertices_of G1

C is Relation-like Function-like FinSequence-like Walk of x

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

x is Element of the_Vertices_of G1

y9 is Relation-like Function-like FinSequence-like Walk of G1

y is Element of the_Vertices_of G1

W is Relation-like Function-like FinSequence-like Walk of G1

y9 .reverse() is Relation-like Function-like FinSequence-like Walk of G1

(y9 .reverse()) .append W is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

(G1,G2) is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

G2 is Element of the_Vertices_of G1

(G1,G2) is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

x is Element of the_Vertices_of G1

y9 is Relation-like Function-like FinSequence-like Walk of G1

y is Element of the_Vertices_of G1

W is Relation-like Function-like FinSequence-like Walk of G1

y9 .reverse() is Relation-like Function-like FinSequence-like Walk of G1

(y9 .reverse()) .append W is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

(G1,G2) is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

x is set

y is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G2 is non empty set

x is Element of the_Vertices_of G1

(G1,x) is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

y is Element of the_Vertices_of G2

(G2,y) is non empty Element of K32((the_Vertices_of G2))

K32((the_Vertices_of G2)) is non empty non empty-membered set

y9 is set

W is Relation-like Function-like FinSequence-like Walk of G1

W9 is Relation-like Function-like FinSequence-like Walk of G2

W is Relation-like Function-like FinSequence-like Walk of G2

W9 is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] () Subgraph of G1

the_Vertices_of G1 is non empty set

the_Vertices_of G2 is non empty set

x is Element of the_Vertices_of G1

y is Element of the_Vertices_of G1

y9 is Element of the_Vertices_of G2

W is Element of the_Vertices_of G2

W9 is Relation-like Function-like FinSequence-like Walk of G2

W9 is Relation-like Function-like FinSequence-like Walk of G1

W is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

(G1) is non empty Element of K32(K32((the_Vertices_of G1)))

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

K32(K32((the_Vertices_of G1))) is non empty non empty-membered set

{(the_Vertices_of G1)} is non empty trivial V31() 1 -element set

the Element of the_Vertices_of G1 is Element of the_Vertices_of G1

x is set

y is Element of the_Vertices_of G1

(G1,y) is non empty Element of K32((the_Vertices_of G1))

(G1, the Element of the_Vertices_of G1) is non empty Element of K32((the_Vertices_of G1))

G2 is Element of the_Vertices_of G1

(G1,G2) is non empty Element of K32((the_Vertices_of G1))

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set

(G1) is non empty Element of K32(K32((the_Vertices_of G1)))

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

K32(K32((the_Vertices_of G1))) is non empty non empty-membered set

(G2) is non empty Element of K32(K32((the_Vertices_of G2)))

the_Vertices_of G2 is non empty set

K32((the_Vertices_of G2)) is non empty non empty-membered set

K32(K32((the_Vertices_of G2))) is non empty non empty-membered set

x is set

y is Element of the_Vertices_of G1

(G1,y) is non empty Element of K32((the_Vertices_of G1))

y9 is Element of the_Vertices_of G2

(G2,y9) is non empty Element of K32((the_Vertices_of G2))

y is Element of the_Vertices_of G2

(G2,y) is non empty Element of K32((the_Vertices_of G2))

y9 is Element of the_Vertices_of G1

(G1,y9) is non empty Element of K32((the_Vertices_of G1))

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

(G1) is non empty Element of K32(K32((the_Vertices_of G1)))

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

K32(K32((the_Vertices_of G1))) is non empty non empty-membered set

G2 is set

x is Element of the_Vertices_of G1

(G1,x) is non empty Element of K32((the_Vertices_of G1))

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) Subgraph of G1

the_Edges_of G2 is Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

the_Vertices_of G2 is non empty Element of K32((the_Vertices_of G1))

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

G1 .edgesBetween (the_Vertices_of G2) is Element of K32((the_Edges_of G1))

x is Element of K32((the_Vertices_of G1))

G1 .edgesBetween x is Element of K32((the_Edges_of G1))

G2 .edgesBetween (the_Vertices_of G2) is Element of K32((the_Edges_of G2))

the_Edges_of G2 is set

K32((the_Edges_of G2)) is non empty set

y9 is set

the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,x,G1 .edgesBetween x is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,x,G1 .edgesBetween x

the_Edges_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,x,G1 .edgesBetween x is Element of K32((the_Edges_of G1))

the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,x,G1 .edgesBetween x is non empty Element of K32((the_Vertices_of G1))

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) Subgraph of G1

the_Vertices_of G2 is non empty Element of K32((the_Vertices_of G1))

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

x is Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) Subgraph of G1

the_Vertices_of x is non empty Element of K32((the_Vertices_of G1))

the_Edges_of G2 is Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

G1 .edgesBetween (the_Vertices_of x) is Element of K32((the_Edges_of G1))

the_Edges_of x is Element of K32((the_Edges_of G1))

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

the_Vertices_of G1 is non empty set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) Subgraph of G1

the_Vertices_of G2 is non empty Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

x is Element of the_Vertices_of G1

(G1,x) is non empty Element of K32((the_Vertices_of G1))

y is set

the_Vertices_of G2 is non empty set

y9 is Element of the_Vertices_of G2

W is Relation-like Function-like FinSequence-like Walk of G2

W9 is Relation-like Function-like FinSequence-like Walk of G1

y9 is Element of the_Vertices_of G1

(G1,y9) is non empty Element of K32((the_Vertices_of G1))

G1 .edgesBetween (G1,y9) is Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

the Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) inducedSubgraph of G1,(G1,y9),G1 .edgesBetween (G1,y9) is Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) inducedSubgraph of G1,(G1,y9),G1 .edgesBetween (G1,y9)

the_Edges_of the Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) inducedSubgraph of G1,(G1,y9),G1 .edgesBetween (G1,y9) is Element of K32((the_Edges_of G1))

the_Source_of G2 is Relation-like Function-like V27( the_Edges_of G2) V28( the_Edges_of G2, the_Vertices_of G2) Element of K32(K33((the_Edges_of G2),(the_Vertices_of G2)))

the_Edges_of G2 is set

K33((the_Edges_of G2),(the_Vertices_of G2)) is Relation-like set

K32(K33((the_Edges_of G2),(the_Vertices_of G2))) is non empty set

W9 is set

(the_Source_of G2) . W9 is set

the_Target_of G2 is Relation-like Function-like V27( the_Edges_of G2) V28( the_Edges_of G2, the_Vertices_of G2) Element of K32(K33((the_Edges_of G2),(the_Vertices_of G2)))

(the_Target_of G2) . W9 is set

the_Edges_of G2 is Element of K32((the_Edges_of G1))

v is Element of the_Vertices_of G2

u9 is Element of the_Vertices_of G2

v9 is Relation-like Function-like FinSequence-like Walk of G2

P is Relation-like Function-like FinSequence-like Walk of G2

P is Relation-like Function-like FinSequence-like Walk of G1

C is Relation-like Function-like FinSequence-like Walk of G1

the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) inducedSubgraph of G1,(G1,y9),G1 .edgesBetween (G1,y9) is non empty Element of K32((the_Vertices_of G1))

W9 is set

W9 is Relation-like Function-like FinSequence-like Walk of G2

W is Relation-like Function-like FinSequence-like Walk of G1

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

G2 is Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) Subgraph of G1

the_Vertices_of G2 is non empty Element of K32((the_Vertices_of G1))

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

x is Relation-like NAT -defined Function-like V31() [Graph-like] () (G1) Subgraph of G1

the_Vertices_of x is non empty Element of K32((the_Vertices_of G1))

y is set

y9 is Element of the_Vertices_of G1

(G1,y9) is non empty Element of K32((the_Vertices_of G1))

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set

(G1) is epsilon-transitive epsilon-connected ordinal cardinal set

(G1) is non empty Element of K32(K32((the_Vertices_of G1)))

the_Vertices_of G1 is non empty set

K32((the_Vertices_of G1)) is non empty non empty-membered set

K32(K32((the_Vertices_of G1))) is non empty non empty-membered set

card (G1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

{(the_Vertices_of G1)} is non empty trivial V31() 1 -element set

G2 is set

{G2} is non empty trivial V31() 1 -element set

x is set

y is Element of the_Vertices_of G1

(G1,y) is non empty Element of K32((the_Vertices_of G1))

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] () set

the_Vertices_of G1 is non empty set

(G1) is epsilon-transitive epsilon-connected ordinal cardinal set

(G1) is non empty Element of K32(K32((the_Vertices_of G1)))

K32((the_Vertices_of G1)) is non empty non empty-membered set

K32(K32((the_Vertices_of G1))) is non empty non empty-membered set

card (G1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

G2 is Element of the_Vertices_of G1

{G2} is non empty trivial V31() 1 -element set

(the_Vertices_of G1) \ {G2} is Element of K32((the_Vertices_of G1))

G1 .edgesBetween ((the_Vertices_of G1) \ {G2}) is Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

x is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is non empty Element of K32(K32((the_Vertices_of x)))

the_Vertices_of x is non empty set

K32((the_Vertices_of x)) is non empty non empty-membered set

K32(K32((the_Vertices_of x))) is non empty non empty-membered set

card (x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

y is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})

(y) is epsilon-transitive epsilon-connected ordinal cardinal set

(y) is non empty Element of K32(K32((the_Vertices_of y)))

the_Vertices_of y is non empty set

K32((the_Vertices_of y)) is non empty non empty-membered set

K32(K32((the_Vertices_of y))) is non empty non empty-membered set

card (y) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2}) is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})

( the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})) is epsilon-transitive epsilon-connected ordinal cardinal set

( the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})) is non empty Element of K32(K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2}))))

the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2}) is non empty set

K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2}))) is non empty non empty-membered set

K32(K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})))) is non empty non empty-membered set

card ( the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is non empty Element of K32(K32((the_Vertices_of x)))

the_Vertices_of x is non empty set

K32((the_Vertices_of x)) is non empty non empty-membered set

K32(K32((the_Vertices_of x))) is non empty non empty-membered set

card (x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] () set

the_Vertices_of G1 is non empty set

G2 is Element of the_Vertices_of G1

{G2} is non empty trivial V31() 1 -element set

(the_Vertices_of G1) \ {G2} is Element of K32((the_Vertices_of G1))

K32((the_Vertices_of G1)) is non empty non empty-membered set

G1 .edgesBetween ((the_Vertices_of G1) \ {G2}) is Element of K32((the_Edges_of G1))

the_Edges_of G1 is set

K32((the_Edges_of G1)) is non empty set

x is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})

(G1) is epsilon-transitive epsilon-connected ordinal cardinal set

(G1) is non empty Element of K32(K32((the_Vertices_of G1)))

K32(K32((the_Vertices_of G1))) is non empty non empty-membered set

card (G1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is non empty Element of K32(K32((the_Vertices_of x)))

the_Vertices_of x is non empty set

K32((the_Vertices_of x)) is non empty non empty-membered set

K32(K32((the_Vertices_of x))) is non empty non empty-membered set

card (x) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set

{{}} is non empty trivial functional V31() V35() 1 -element set

{} \/ {{}} is non empty V31() V35() set

G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite non trivial () set

the_Vertices_of G1 is non empty V31() set

G2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set

x is Relation-like NAT -defined Function-like V31() [Graph-like] finite non trivial () set

x .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

(x) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

(x) is non empty V31() V35() Element of K32(K32((the_Vertices_of x)))

the_Vertices_of x is non empty V31() set

K32((the_Vertices_of x)) is non empty non empty-membered V31() V35() set

K32(K32((the_Vertices_of x))) is non empty non empty-membered V31() V35() set

card (x) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set

y is Element of the_Vertices_of x

y9 is Element of the_Vertices_of x

W is Element of the_Vertices_of x

W9 is Element of the_Vertices_of x

y is Element of the_Vertices_of x

y is Element of the_Vertices_of x

{y} is non empty trivial V31() 1 -element set

(the_Vertices_of x) \ {y} is V31() Element of K32((the_Vertices_of x))

x .edgesBetween ((the_Vertices_of x) \ {y}) is V31() Element of K32((the_Edges_of x))

the_Edges_of x is V31() set

K32((the_Edges_of x)) is non empty V31() V35() set

the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) is Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})

( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})) is non empty V31() V35() Element of K32(K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}))))

the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) is non empty V31() set

K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}))) is non empty non empty-membered V31() V35() set

K32(K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})))) is non empty non empty-membered V31() V35() set

card ( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set

1 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

card 2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

card ( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

W is set

W9 is set

W9 is V31() Element of ( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}))

the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) .edgesBetween W9 is V31() Element of K32((the_Edges_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})))

the_Edges_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) is V31() set

K32((the_Edges_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}))) is non empty V31() V35() set

the Relation-like NAT -defined Function-like V31() [Graph-like] finite () ( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})) inducedSubgraph of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}),W9, the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) .edgesBetween W9 is Relation-like NAT -defined Function-like V31() [Graph-like] finite () ( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})) inducedSubgraph of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}),W9, the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) .edgesBetween W9

W is V31() Element of ( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}))

the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) .edgesBetween W is V31() Element of K32((the_Edges_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})))

the Relation-like NAT -defined Function-like V31() [Graph-like] finite () ( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})) inducedSubgraph of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}),W, the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) .edgesBetween W is Relation-like NAT -defined Function-like V31() [Graph-like] finite () ( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})) inducedSubgraph of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}),W, the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) .edgesBetween W

the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) is non empty V31() Element of K32((the_Vertices_of x))

{y} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of x))

(the_Vertices_of x) \ {y} is V31() Element of K32((the_Vertices_of x))

x .edgesBetween ((the_Vertices_of x) \ {y}) is V31() Element of K32((the_Edges_of x))

x .edgesInOut {y} is V31() Element of K32((the_Edges_of x))

(the_Edges_of x) \ (x .edgesInOut {y}) is V31() Element of K32((the_Edges_of x))

y .edgesInOut() is V31() Element of K32((the_Edges_of x))

(the_Edges_of x) \ (y .edgesInOut()) is V31() Element of K32((the_Edges_of x))

the_Edges_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) is V31() Element of K32((the_Edges_of x))

the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}) .order()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

v9 is Relation-like NAT -defined Function-like V31() [Graph-like] finite () ( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})) Subgraph of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})

the_Vertices_of v9 is non empty V31() set

the Element of the_Vertices_of v9 is Element of the_Vertices_of v9

the_Vertices_of v9 is non empty V31() Element of K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})))

P is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})

P is Element of the_Vertices_of x

P is Relation-like Function-like FinSequence-like Walk of x

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P is Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P .first() is Element of the_Vertices_of x

2 * 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

(2 * 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P .cut (((2 * 1) + 1),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P)) is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of x

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P .last() is Element of the_Vertices_of x

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P . (len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P) is set

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P . 3 is set

2 * 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P . ((2 * 0) + 1) is set

( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P .cut (((2 * 1) + 1),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P))) .vertices() is V31() Element of K32((the_Vertices_of x))

len ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P .cut (((2 * 1) + 1),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P))) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

P2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P .cut (((2 * 1) + 1),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P))) . P2 is set

P2 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

1 + 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

dom ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P .cut (((2 * 1) + 1),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P))) is Element of K32(NAT)

3 + P2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

(3 + P2) - 1 is V46() V47() V95() ext-real set

dom the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P is Element of K32(NAT)

2 + P2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P . ((3 + P2) - 1) is set

P2 is Relation-like Function-like FinSequence-like Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})

P2 .reverse() is Relation-like Function-like FinSequence-like Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})

( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}),P) is non empty V31() Element of K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})))

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P . 1 is set

1 + 2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P . (1 + 2) is set

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P . (1 + 1) is set

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of P . 2 is set

C is Element of the_Vertices_of v9

P is set

C is Element of the_Vertices_of v9

P is set

P is Element of the_Vertices_of v9

{P} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of v9))

K32((the_Vertices_of v9)) is non empty non empty-membered V31() V35() set

P is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})

m is Element of the_Vertices_of x

P1 is Element of the_Vertices_of x

{P} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})))

( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y}),P) is non empty V31() Element of K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})))

{P1} is non empty trivial V31() 1 -element set

(the_Vertices_of x) \ {P1} is V31() Element of K32((the_Vertices_of x))

x .edgesBetween ((the_Vertices_of x) \ {P1}) is V31() Element of K32((the_Edges_of x))

the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1}) is Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

P29 is set

P19 is set

the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1}) is non empty V31() set

P19 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

P29 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1}) .walkOf P19 is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

b is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

P19 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

P29 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

a is Element of the_Vertices_of x

b is Element of the_Vertices_of x

v is Relation-like Function-like FinSequence-like Walk of x

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v is Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v

the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1}) is non empty V31() Element of K32((the_Vertices_of x))

{P1} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of x))

(the_Vertices_of x) \ {P1} is V31() Element of K32((the_Vertices_of x))

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v . 1 is set

len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v . (len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v) is set

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v .vertices() is V31() Element of K32((the_Vertices_of x))

cv9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v . cv9 is set

cv9 - (2 * 1) is non empty V46() V47() non even V95() ext-real set

cv9 - 0 is V46() V47() V95() ext-real set

y is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v . y is set

y + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v . (y + 1) is set

cv9 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v . (cv9 + 1) is set

(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v) - 0 is V46() V47() V95() ext-real set

cv9 - 2 is V46() V47() V95() ext-real set

y + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v . (y + 2) is set

cv9 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT

cv9 + 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of v . (cv9 + 2) is set

y + 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

cv9 is Relation-like Function-like FinSequence-like Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

y is Relation-like Function-like FinSequence-like Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

P19 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

P29 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

P19 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

P29 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

a is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})

( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT

( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})) is non empty V31() V35() Element of K32(K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1}))))

K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1}))) is non empty non empty-membered V31() V35() set

K32(K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {P1},x .edgesBetween ((