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 ((the_Vertices_of x) \ {P1})))) 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) \ {P1},x .edgesBetween ((the_Vertices_of x) \ {P1})) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
v9 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(v9 .order()) + 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
P is Relation-like NAT -defined Function-like V31() [Graph-like] non trivial set
the_Vertices_of P is non empty set
P is Element of the_Vertices_of P
m is Element of the_Vertices_of P
{P} is non empty trivial V31() 1 -element set
(the_Vertices_of P) \ {P} is Element of K32((the_Vertices_of P))
K32((the_Vertices_of P)) is non empty non empty-membered set
P .edgesBetween ((the_Vertices_of P) \ {P}) is Element of K32((the_Edges_of P))
the_Edges_of P is set
K32((the_Edges_of P)) is non empty set
the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P}) is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P})
{m} is non empty trivial V31() 1 -element set
(the_Vertices_of P) \ {m} is Element of K32((the_Vertices_of P))
P .edgesBetween ((the_Vertices_of P) \ {m}) is Element of K32((the_Edges_of P))
the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {m},P .edgesBetween ((the_Vertices_of P) \ {m}) is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {m},P .edgesBetween ((the_Vertices_of P) \ {m})
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P}) is non empty Element of K32((the_Vertices_of P))
{P} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of P))
(the_Vertices_of P) \ {P} is Element of K32((the_Vertices_of P))
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {m},P .edgesBetween ((the_Vertices_of P) \ {m}) is non empty Element of K32((the_Vertices_of P))
{m} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of P))
(the_Vertices_of P) \ {m} is Element of K32((the_Vertices_of P))
y .allNeighbors() is V31() Element of K32((the_Vertices_of x))
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) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})
P29 is Element of the_Vertices_of x
a is Element of the_Vertices_of x
{a} is non empty trivial V31() 1 -element set
(the_Vertices_of x) \ {a} is V31() Element of K32((the_Vertices_of x))
x .edgesBetween ((the_Vertices_of x) \ {a}) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) is Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) is non empty V31() Element of K32((the_Vertices_of x))
{a} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of x))
(the_Vertices_of x) \ {a} is V31() Element of K32((the_Vertices_of x))
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) is non empty V31() 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}),P19) 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})))
G3 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) .walkOf G3 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
G3 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
cv9 is Relation-like Function-like FinSequence-like Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P})
cv9 . 1 is set
len cv9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
cv9 . (len cv9) is set
cv9 .vertices() is V31() Element of K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P})))
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P}) is non empty set
K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P}))) is non empty non empty-membered set
a .edgesInOut() is V31() Element of K32((the_Edges_of x))
(the_Edges_of x) \ (a .edgesInOut()) is V31() Element of K32((the_Edges_of x))
x .edgesInOut {a} is V31() Element of K32((the_Edges_of x))
(the_Edges_of x) \ (x .edgesInOut {a}) is V31() Element of K32((the_Edges_of x))
x .edgesBetween ((the_Vertices_of x) \ {a}) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) is V31() Element of K32((the_Edges_of x))
y is Relation-like Function-like FinSequence-like Walk of v9
y9 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})
W is Relation-like Function-like FinSequence-like Walk of x
W .vertices() is V31() Element of K32((the_Vertices_of x))
P 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
P .addEdge P 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
(P .addEdge P) .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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
cv9 is Element of the_Vertices_of x
y is Relation-like Function-like FinSequence-like Walk of x
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y is Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y
len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of 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 y . (len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y) is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y . 1 is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y .vertices() is V31() Element of K32((the_Vertices_of x))
W 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 y . W is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y)) 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 y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y))) .vertices() is V31() Element of K32((the_Vertices_of x))
len ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y))) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
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 y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y))) . P is set
dom ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y))) is Element of K32(NAT)
W + P is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
(W + P) - 1 is non empty V46() V47() non even V95() ext-real set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y . ((W + P) - 1) is set
(1 + 1) - 1 is V46() V47() V95() ext-real set
dom the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y is Element of K32(NAT)
P 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})
W 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
P 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
G3 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
G3 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}))))
K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}))) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})))) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
y .allNeighbors() is V31() Element of K32((the_Vertices_of x))
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) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})
P29 is Element of the_Vertices_of x
a is Element of the_Vertices_of x
{a} is non empty trivial V31() 1 -element set
(the_Vertices_of x) \ {a} is V31() Element of K32((the_Vertices_of x))
x .edgesBetween ((the_Vertices_of x) \ {a}) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) is Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) is non empty V31() Element of K32((the_Vertices_of x))
{a} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of x))
(the_Vertices_of x) \ {a} is V31() Element of K32((the_Vertices_of x))
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) is non empty V31() 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}),P19) 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})))
G3 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) .walkOf G3 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
G3 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
cv9 is Relation-like Function-like FinSequence-like Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {m},P .edgesBetween ((the_Vertices_of P) \ {m})
cv9 . 1 is set
len cv9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
cv9 . (len cv9) is set
cv9 .vertices() is V31() Element of K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {m},P .edgesBetween ((the_Vertices_of P) \ {m})))
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {m},P .edgesBetween ((the_Vertices_of P) \ {m}) is non empty set
K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {m},P .edgesBetween ((the_Vertices_of P) \ {m}))) is non empty non empty-membered set
a .edgesInOut() is V31() Element of K32((the_Edges_of x))
(the_Edges_of x) \ (a .edgesInOut()) is V31() Element of K32((the_Edges_of x))
x .edgesInOut {a} is V31() Element of K32((the_Edges_of x))
(the_Edges_of x) \ (x .edgesInOut {a}) is V31() Element of K32((the_Edges_of x))
x .edgesBetween ((the_Vertices_of x) \ {a}) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}) is V31() Element of K32((the_Edges_of x))
y is Relation-like Function-like FinSequence-like Walk of v9
y9 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})
W is Relation-like Function-like FinSequence-like Walk of x
W .vertices() is V31() Element of K32((the_Vertices_of x))
P 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
P .addEdge P 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
(P .addEdge P) .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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
cv9 is Element of the_Vertices_of x
y is Relation-like Function-like FinSequence-like Walk of x
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y is Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y
len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of 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 y . (len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y) is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y . 1 is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y .vertices() is V31() Element of K32((the_Vertices_of x))
W 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 y . W is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y)) 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 y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y))) .vertices() is V31() Element of K32((the_Vertices_of x))
len ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y))) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
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 y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y))) . P is set
dom ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y .cut (W,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y))) is Element of K32(NAT)
W + P is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
(W + P) - 1 is non empty V46() V47() non even V95() ext-real set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y . ((W + P) - 1) is set
(1 + 1) - 1 is V46() V47() V95() ext-real set
dom the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of y is Element of K32(NAT)
P 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})
W 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
P 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
G3 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
v is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
G3 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})
( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}))))
K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a}))) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})))) 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) \ {a},x .edgesBetween ((the_Vertices_of x) \ {a})) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
y .allNeighbors() is V31() Element of K32((the_Vertices_of x))
P19 is set
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) \ {y},x .edgesBetween ((the_Vertices_of x) \ {y})
b is Element of the_Vertices_of x
v is Element of the_Vertices_of x
{v} is non empty trivial V31() 1 -element set
(the_Vertices_of x) \ {v} is V31() Element of K32((the_Vertices_of x))
x .edgesBetween ((the_Vertices_of x) \ {v}) 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v}) is Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v}) is non empty V31() Element of K32((the_Vertices_of x))
{v} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of x))
(the_Vertices_of x) \ {v} is V31() Element of K32((the_Vertices_of x))
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v}) is non empty V31() 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}),P29) 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})))
y is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
cv9 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v}) .walkOf y 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
y is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
y9 is Relation-like Function-like FinSequence-like Walk of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P})
y9 . 1 is set
len y9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
y9 . (len y9) is set
y9 .vertices() is V31() Element of K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P})))
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P}) is non empty set
K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of P,(the_Vertices_of P) \ {P},P .edgesBetween ((the_Vertices_of P) \ {P}))) is non empty non empty-membered set
v .edgesInOut() is V31() Element of K32((the_Edges_of x))
(the_Edges_of x) \ (v .edgesInOut()) is V31() Element of K32((the_Edges_of x))
x .edgesInOut {v} is V31() Element of K32((the_Edges_of x))
(the_Edges_of x) \ (x .edgesInOut {v}) is V31() Element of K32((the_Edges_of x))
x .edgesBetween ((the_Vertices_of x) \ {v}) 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v}) is V31() Element of K32((the_Edges_of x))
W is Relation-like Function-like FinSequence-like Walk of v9
P 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})
P is Relation-like Function-like FinSequence-like Walk of x
P .vertices() is V31() Element of K32((the_Vertices_of x))
P 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
P .addEdge P19 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
(P .addEdge P19) .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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
cv9 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
y9 is Element of the_Vertices_of x
W is Relation-like Function-like FinSequence-like Walk of x
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W is Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W
len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W 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 W . (len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W) is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W . 1 is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W .vertices() is V31() Element of K32((the_Vertices_of x))
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 W . P is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W .cut (P,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W)) 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 W .cut (P,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W))) .vertices() is V31() Element of K32((the_Vertices_of x))
len ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W .cut (P,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W))) 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 W .cut (P,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W))) . P2 is set
dom ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W .cut (P,(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W))) is Element of K32(NAT)
P + P2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
(P + P2) - 1 is non empty V46() V47() non even V95() ext-real set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W . ((P + P2) - 1) is set
(1 + 1) - 1 is V46() V47() V95() ext-real set
dom the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of W is Element of K32(NAT)
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})
P 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
cv9 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
P 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
cv9 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
cv9 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
y9 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
y is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
cv9 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
cv9 is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
y is Element of the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
y9 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})
( the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})) 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})) 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v}))))
K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of x,(the_Vertices_of x) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v}))) 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})))) 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) \ {v},x .edgesBetween ((the_Vertices_of x) \ {v})) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
y .allNeighbors() is V31() Element of K32((the_Vertices_of x))
P19 is Element of the_Vertices_of x
P is Element of the_Vertices_of x
the_Vertices_of 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 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})))
v9 is Element of the_Vertices_of x
the_Vertices_of 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 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})))
C is Element of the_Vertices_of x
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
P is Element of the_Vertices_of x
P is Element of the_Vertices_of x
y is Element of the_Vertices_of x
y is Element of the_Vertices_of x
y9 is Element of the_Vertices_of x
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
the_Vertices_of x 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
the_Vertices_of x is non empty V31() set
G1 .order() 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] finite non trivial () set
the_Vertices_of G1 is non empty V31() set
G2 is Element of the_Vertices_of G1
x is Element of the_Vertices_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 Function-like FinSequence-like Trail-like Path-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
G2 .last() is Element of the_Vertices_of G1
the_Vertices_of G1 is non empty set
(G2 .last()) .edgesInOut() is Element of K32((the_Edges_of G1))
x is set
G2 .addEdge x is Relation-like Function-like FinSequence-like Walk of G1
(G2 .last()) .adj x is Element of the_Vertices_of G1
len (G2 .addEdge x) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
len G2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
(len G2) + 2 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
G2 . W 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 .addEdge x) .cut (W,(len (G2 .addEdge x))) is Relation-like Function-like FinSequence-like Walk of G1
G2 . W is set
((G2 .addEdge x) .cut (W,(len (G2 .addEdge x)))) .first() is Element of the_Vertices_of G1
(G2 .addEdge x) . W is set
len ((G2 .addEdge x) .cut (W,(len (G2 .addEdge x)))) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
1 + W is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
(len (G2 .addEdge x)) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
2 + (len G2) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
(2 + (len G2)) - (len G2) is V46() V47() even V95() ext-real set
(len G2) - (len G2) is V46() V47() even V95() ext-real set
W9 is Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of (G2 .addEdge x) .cut (W,(len (G2 .addEdge x)))
((G2 .addEdge x) .cut (W,(len (G2 .addEdge x)))) .last() is Element of the_Vertices_of G1
(G2 .addEdge x) . (len (G2 .addEdge x)) is set
(G2 .addEdge x) .last() is Element of the_Vertices_of G1
dom G2 is Element of K32(NAT)
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non trivial non-multi non-Dmulti simple Dsimple () set
the_Edges_of G1 is V31() set
the_Vertices_of G1 is non empty V31() set
choose (the_Edges_of G1) is Element of the_Edges_of G1
x is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
y is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
len y is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
y is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
len y is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
y .vertexSeq() is Relation-like Function-like FinSequence-like VertexSeq of G1
len (y .vertexSeq()) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
2 * (len (y .vertexSeq())) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
G1 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G1 .order()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
2 * ((G1 .order()) + 1) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
x + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(x + 1) - 1 is V46() V47() V95() ext-real set
(2 * ((G1 .order()) + 1)) - 0 is V46() V47() V95() ext-real set
the_Source_of G1 is Relation-like Function-like V27( the_Edges_of G1) V28( the_Edges_of G1, the_Vertices_of G1) V31() Element of K32(K33((the_Edges_of G1),(the_Vertices_of G1)))
K33((the_Edges_of G1),(the_Vertices_of G1)) is Relation-like V31() set
K32(K33((the_Edges_of G1),(the_Vertices_of G1))) is non empty V31() V35() set
(the_Source_of G1) . (choose (the_Edges_of G1)) is set
the_Target_of G1 is Relation-like Function-like V27( the_Edges_of G1) V28( the_Edges_of G1, the_Vertices_of G1) V31() Element of K32(K33((the_Edges_of G1),(the_Vertices_of G1)))
(the_Target_of G1) . (choose (the_Edges_of G1)) is set
G1 .walkOf (((the_Source_of G1) . (choose (the_Edges_of G1))),(choose (the_Edges_of G1)),((the_Target_of G1) . (choose (the_Edges_of G1)))) is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
len (G1 .walkOf (((the_Source_of G1) . (choose (the_Edges_of G1))),(choose (the_Edges_of G1)),((the_Target_of G1) . (choose (the_Edges_of G1))))) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
y9 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
W is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
len W is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
W is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
len W is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
W .reverse() is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
len (W .reverse()) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
W .first() is Element of the_Vertices_of G1
W .last() is Element of the_Vertices_of G1
W9 is Relation-like Function-like FinSequence-like Trail-like Path-like Walk 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
2 + 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
(len W9) - (2 * 1) is non empty V46() V47() non even V95() ext-real set
W9 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
W9 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
W9 .last() is Element of the_Vertices_of G1
W9 .vertices() is V31() Element of K32((the_Vertices_of G1))
K32((the_Vertices_of G1)) is non empty non empty-membered V31() V35() set
(W9 .last()) .degree() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(W9 .last()) .edgesInOut() is V31() Element of K32((the_Edges_of G1))
K32((the_Edges_of G1)) is non empty V31() V35() set
card ((W9 .last()) .edgesInOut()) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
W is set
v is set
W9 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
W9 . (W9 + 1) is set
u9 is set
W9 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
W9 . (W9 + 1) is set
u9 is set
W9 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
W9 . (W9 + 1) is set
W9 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
W9 . (W9 + 1) is set
u9 is set
u9 is set
v9 is Element of the_Vertices_of G1
C is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
W9 . C is set
W9 .rfind C is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
W9 .cut ((W9 .rfind C),(len W9)) is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
(W9 .cut ((W9 .rfind C),(len W9))) .last() is Element of the_Vertices_of G1
W9 . (len W9) is set
W9 . (W9 .rfind C) is set
(W9 .cut ((W9 .rfind C),(len W9))) .first() is Element of the_Vertices_of G1
((W9 .cut ((W9 .rfind C),(len W9))) .last()) .edgesInOut() is V31() Element of K32((the_Edges_of G1))
(W9 .cut ((W9 .rfind C),(len W9))) .edges() is V31() Element of K32((the_Edges_of G1))
(W9 .cut ((W9 .rfind C),(len W9))) .addEdge u9 is Relation-like Function-like FinSequence-like Walk of G1
((W9 .cut ((W9 .rfind C),(len W9))) .addEdge u9) .first() is Element of the_Vertices_of G1
((W9 .cut ((W9 .rfind C),(len W9))) .addEdge u9) .last() is Element of the_Vertices_of G1
(W9 .cut ((W9 .rfind C),(len W9))) .edges() is V31() Element of K32((the_Edges_of G1))
W9 .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
W9 . P is set
P - 1 is non empty V46() V47() non even V95() ext-real set
(len W9) - 0 is V46() V47() V95() ext-real set
m is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
(W9 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
m + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
W9 . m is set
m + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
W9 . (m + 2) is set
(W9 + 1) - 1 is non empty V46() V47() non even V95() ext-real set
(W9 .cut ((W9 .rfind C),(len W9))) .edges() is V31() Element of K32((the_Edges_of G1))
W9 .addEdge u9 is Relation-like Function-like FinSequence-like Walk of G1
len (W9 .addEdge u9) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
y9 + 2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
y9 + 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G1,(W .first())) is non empty V31() Element of K32((the_Vertices_of G1))
(W .reverse()) .last() is Element of the_Vertices_of G1
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non trivial non-multi non-Dmulti simple Dsimple () () () set
the_Vertices_of G1 is non empty V31() set
G2 is Element of the_Vertices_of G1
x is Element of the_Vertices_of G1
y is Relation-like Function-like FinSequence-like Walk of G1
len y is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
y .last() is Element of the_Vertices_of G1
y . 1 is set
y .first() is Element of the_Vertices_of G1
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
dom y is Element of K32(NAT)
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
y . (2 * 1) is set
the_Edges_of G1 is V31() set
y9 is Element of the_Vertices_of G1
W is Element of the_Vertices_of G1
(G1,y9) is non empty V31() Element of K32((the_Vertices_of G1))
K32((the_Vertices_of G1)) is non empty non empty-membered V31() V35() set
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non trivial non-multi non-Dmulti simple Dsimple () () () set
the_Vertices_of G1 is non empty V31() set
G2 is Element of the_Vertices_of G1
x is Element of the_Vertices_of G1
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non trivial non-multi non-Dmulti simple Dsimple () () () set
the_Vertices_of G1 is non empty V31() set
G2 is endvertex 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
x is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () inducedSubgraph of G1,(the_Vertices_of G1) \ {G2},G1 .edgesBetween ((the_Vertices_of G1) \ {G2})
G1 is Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding set
G2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
G1 . G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set
x is Relation-like NAT -defined Function-like V31() [Graph-like] trivial () set
G1 is Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding set
G2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
G1 . G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set
x is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless trivial non-multi non-Dmulti simple Dsimple () () () set
G1 is Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding set
G2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
G1 . G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set
x is Relation-like NAT -defined Function-like V31() [Graph-like] loopless non-multi non-Dmulti simple Dsimple () set
G1 is Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding set
G2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
G1 . G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set
x is Relation-like NAT -defined Function-like V31() [Graph-like] loopless non-multi non-Dmulti simple Dsimple () () () set
G1 is Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding set
G2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
G1 . G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set
x is Relation-like NAT -defined Function-like V31() [Graph-like] loopless non-multi non-Dmulti simple Dsimple () () () set
the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set
NAT --> the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set is non empty Relation-like NAT -defined Function-like constant V27( NAT ) V28( NAT ,{ the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set }) Function-yielding V81() Element of K32(K33(NAT,{ the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set }))
{ the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set } is non empty trivial functional V31() V35() 1 -element set
K33(NAT,{ the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set }) is non empty non trivial Relation-like V31() set
K32(K33(NAT,{ the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set })) is non empty non trivial non empty-membered V31() set
dom (NAT --> the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set ) is non empty set
y is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
x is Relation-like NAT -defined Function-like V27( NAT ) set
x . y is set
rng x is set
y is Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
y . (1 + 1) is Relation-like NAT -defined Function-like V31() [Graph-like] set
rng y is set
y . 1 is Relation-like NAT -defined Function-like V31() [Graph-like] set
y9 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
y . y9 is Relation-like NAT -defined Function-like V31() [Graph-like] set
G1 is Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding () set
G2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
G1 . G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set
x is Relation-like NAT -defined Function-like V31() [Graph-like] set
G1 is Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding loopless non-multi non-Dmulti simple Dsimple () set
G2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
G1 . G2 is Relation-like NAT -defined Function-like V31() [Graph-like] loopless non-multi non-Dmulti simple Dsimple set
x is Relation-like NAT -defined Function-like V31() [Graph-like] set
G1 is Relation-like NAT -defined Function-like V27( NAT ) Graph-yielding loopless non-multi non-Dmulti simple Dsimple () () () set
G2 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
G1 . G2 is Relation-like NAT -defined Function-like V31() [Graph-like] loopless non-multi non-Dmulti simple Dsimple () () () set
x is Relation-like NAT -defined Function-like V31() [Graph-like] set
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
x is Element of the_Vertices_of G1
y is Element of the_Vertices_of G1
y9 is Element of the_Vertices_of G1
y9 is Element of the_Vertices_of G1
W is Relation-like Function-like FinSequence-like Walk of G1
W .first() is Element of the_Vertices_of G1
W .last() is Element of the_Vertices_of G1
W .vertices() is V31() Element of K32((the_Vertices_of G1))
K32((the_Vertices_of G1)) is non empty non empty-membered set
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
G2 .edgesInOut() is Element of K32((the_Edges_of G1))
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})
y is Element of the_Vertices_of G1
{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_Vertices_of x is non empty Element of K32((the_Vertices_of G1))
y is set
y is set
G2 .adj y is Element of the_Vertices_of G1
the_Vertices_of x is non empty set
W9 is Element of the_Vertices_of G1
W9 is Element of the_Vertices_of G1
W is Element of the_Vertices_of x
v is Element of the_Vertices_of x
u9 is Relation-like Function-like FinSequence-like Walk of x
v9 is Relation-like Function-like FinSequence-like Walk of G1
W9 is Element of the_Vertices_of G1
W is Element of the_Vertices_of x
W is Element of the_Vertices_of x
v is Relation-like Function-like FinSequence-like Walk of x
u9 is Relation-like Function-like FinSequence-like Walk of G1
u9 .first() is Element of the_Vertices_of G1
u9 .last() is Element of the_Vertices_of G1
u9 .addEdge y is Relation-like Function-like FinSequence-like Walk of G1
W9 is Element of the_Vertices_of G1
W9 is Element of the_Vertices_of G1
v is Relation-like Function-like FinSequence-like Walk of G1
W9 is Element of the_Vertices_of G1
W9 is Element of the_Vertices_of G1
G1 .walkOf (W9,y,(G2 .adj y)) is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
W is Element of the_Vertices_of x
W is Element of the_Vertices_of x
u9 is Relation-like Function-like FinSequence-like Walk of x
v9 is Relation-like Function-like FinSequence-like Walk of G1
(G1 .walkOf (W9,y,(G2 .adj y))) .append v9 is Relation-like Function-like FinSequence-like Walk of G1
C is Relation-like Function-like FinSequence-like Walk of G1
W9 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
W is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of G1
W9 is Element of the_Vertices_of G1
W9 is Element of the_Vertices_of G1
W is Relation-like Function-like FinSequence-like Walk of G1
W9 is Element of the_Vertices_of G1
W9 is Element of the_Vertices_of G1
W9 is Element of the_Vertices_of G1
W9 is Element of the_Vertices_of G1
W is Relation-like Function-like FinSequence-like Walk of G1
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})
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] () set
the_Vertices_of G1 is non empty set
the_Edges_of G1 is set
G2 is Relation-like Function-like FinSequence-like Walk of G1
G2 .edges() is V31() Element of K32((the_Edges_of G1))
K32((the_Edges_of G1)) is non empty set
x is set
{x} is non empty trivial V31() 1 -element set
(the_Edges_of G1) \ {x} is Element of K32((the_Edges_of G1))
y is Relation-like NAT -defined Function-like V31() [Graph-like] spanning inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ {x}
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)))
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_Source_of G1) . x is 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)))
(the_Target_of G1) . x is set
y9 is Element of the_Vertices_of G1
W is Element of the_Vertices_of G1
W9 is Relation-like Function-like FinSequence-like Walk of G1
W9 .edges() is V31() Element of K32((the_Edges_of G1))
W9 is Relation-like Function-like FinSequence-like Walk of y
W9 .reverse() is Relation-like Function-like FinSequence-like Walk of y
the_Vertices_of y is non empty set
the_Vertices_of y is non empty Element of K32((the_Vertices_of G1))
K32((the_Vertices_of G1)) is non empty non empty-membered set
W is Element of the_Vertices_of y
v is Element of the_Vertices_of y
u9 is Element of the_Vertices_of G1
v9 is Element of the_Vertices_of G1
C is Relation-like Function-like FinSequence-like Walk of G1
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C is Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C
len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C 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 C . (len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C) is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C . 1 is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .edges() is V31() Element of K32((the_Edges_of G1))
m is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
m + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
P is Element of the_Vertices_of G1
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C . m is set
m + 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 C . (m + 1) is set
P is Element of the_Vertices_of G1
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C . (m + 2) is set
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .cut (1,m) is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .cut ((m + 2),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C)) is Relation-like Function-like FinSequence-like Trail-like Path-like Walk of G1
(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C) - 0 is V46() V47() V95() ext-real set
(m + 2) - 2 is V46() V47() V95() ext-real set
( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .cut (1,m)) .edges() is V31() Element of K32((the_Edges_of G1))
len ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .cut (1,m)) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
P19 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 C .cut (1,m)) . P19 is set
dom ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .cut (1,m)) is Element of K32(NAT)
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C . P19 is set
( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .cut ((m + 2),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C))) .edges() is V31() Element of K32((the_Edges_of G1))
len ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .cut ((m + 2),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C))) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
P29 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 C .cut ((m + 2),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C))) . P29 is set
P29 - 1 is non empty V46() V47() non even V95() ext-real set
(len ( the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .cut ((m + 2),(len the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C)))) - 0 is V46() V47() V95() ext-real set
a is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
(m + 2) + a is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() even V95() ext-real Element of NAT
dom the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C is Element of K32(NAT)
a + 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 C . ((m + 2) + a) is set
(m + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() non even V95() ext-real Element of NAT
(m + 1) + 0 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
a is Element of the_Vertices_of y
P19 is Relation-like Function-like FinSequence-like Walk of y
b is Element of the_Vertices_of y
P29 is Relation-like Function-like FinSequence-like Walk of y
P19 .append W9 is Relation-like Function-like FinSequence-like Walk of y
(P19 .append W9) .append P29 is Relation-like Function-like FinSequence-like Walk of y
P19 .append (W9 .reverse()) is Relation-like Function-like FinSequence-like Walk of y
(P19 .append (W9 .reverse())) .append P29 is Relation-like Function-like FinSequence-like Walk of y
v is Relation-like Function-like FinSequence-like Walk of y
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .edges() is V31() Element of K32((the_Edges_of G1))
P is Relation-like Function-like FinSequence-like Walk of y
P is Relation-like Function-like FinSequence-like Walk of y
the Relation-like Function-like FinSequence-like Trail-like Path-like Subwalk of C .edges() is V31() Element of K32((the_Edges_of G1))
P is Relation-like Function-like FinSequence-like Walk of y
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 is Relation-like NAT -defined Function-like V31() [Graph-like] trivial () set
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set
G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set
the_Vertices_of G2 is non empty set
the_Vertices_of G1 is non empty set
x is Element of the_Vertices_of G2
y is Element of the_Vertices_of G2
y9 is Element of the_Vertices_of G1
W is Element of the_Vertices_of G1
W9 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
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 is Relation-like NAT -defined Function-like V31() [Graph-like] set
the_Vertices_of G1 is non empty set
G2 is set
y9 is Element of the_Vertices_of G1
(G1,y9) 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
x is 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
(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
G1 .edgesInOut (G1,G2) is Element of K32((the_Edges_of G1))
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)))
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
y is set
(the_Source_of G1) . y is 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)))
(the_Target_of G1) . y is set
W9 is Element of the_Vertices_of G1
W is Relation-like Function-like FinSequence-like Walk of G1
W .last() is Element of the_Vertices_of G1
W9 is Element of the_Vertices_of G1
W .first() is Element of the_Vertices_of G1
W .addEdge y is Relation-like Function-like FinSequence-like Walk of G1
G1 .edgesInto (G1,G2) is Element of K32((the_Edges_of G1))
G1 .edgesOutOf (G1,G2) is Element of K32((the_Edges_of G1))
(G1 .edgesInto (G1,G2)) /\ (G1 .edgesOutOf (G1,G2)) is Element of K32((the_Edges_of G1))
W9 is Element of the_Vertices_of G1
W is Relation-like Function-like FinSequence-like Walk of G1
W .last() is Element of the_Vertices_of G1
W9 is Element of the_Vertices_of G1
W .first() is Element of the_Vertices_of G1
W .addEdge y is Relation-like Function-like FinSequence-like Walk of G1
G1 .edgesOutOf (G1,G2) is Element of K32((the_Edges_of G1))
G1 .edgesInto (G1,G2) is Element of K32((the_Edges_of G1))
(G1 .edgesInto (G1,G2)) /\ (G1 .edgesOutOf (G1,G2)) is Element of K32((the_Edges_of G1))
W9 is Element of the_Vertices_of G1
W9 is 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
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))
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 Relation-like Function-like FinSequence-like Walk of G1
x .vertices() is V31() 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))
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] Subgraph of G1
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 G2
W9 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
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 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
y is Element of the_Vertices_of G2
(G1,x) is non empty Element of K32((the_Vertices_of G1))
K32((the_Vertices_of G1)) is non empty non empty-membered set
(G2,y) is non empty Element of K32((the_Vertices_of G2))
K32((the_Vertices_of G2)) is non empty non empty-membered 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
(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 set
x is set
y is set
y9 is Element of the_Vertices_of G1
(G1,y9) is non empty Element of K32((the_Vertices_of G1))
K32((the_Vertices_of G1)) is non empty non empty-membered set
W9 is Relation-like Function-like FinSequence-like directed 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
(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,G2) is non empty Element of K32((the_Vertices_of G1))
y is set
y9 is Element of the_Vertices_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 Relation-like NAT -defined Function-like V31() [Graph-like] Subgraph of G1
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 directed Walk of G2
W9 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 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 directed Walk of G1
W9 is Relation-like Function-like FinSequence-like directed Walk of G2
W is Relation-like Function-like FinSequence-like directed Walk of G2
W9 is Relation-like Function-like FinSequence-like directed 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
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set
the_Vertices_of G1 is non empty 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
union (G1) is Element of K32((the_Vertices_of G1))
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
(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
G2 is Relation-like NAT -defined Function-like V31() [Graph-like] 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
{(the_Vertices_of G2)} is non empty trivial V31() 1 -element set
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
G2 is set
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
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
G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set
(G2) is epsilon-transitive epsilon-connected ordinal cardinal 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
card (G2) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
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 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
(G2) is epsilon-transitive epsilon-connected ordinal cardinal 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
card (G2) is non empty epsilon-transitive epsilon-connected ordinal cardinal 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
the_Vertices_of G1 is non empty set
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
the_Edges_of G1 is set
the_Edges_of G2 is Element of K32((the_Edges_of G1))
K32((the_Edges_of G1)) is non empty set
the_Vertices_of G1 is non empty set
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
the_Edges_of G1 is set
the_Edges_of G2 is Element of K32((the_Edges_of G1))
K32((the_Edges_of G1)) is non empty set
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))
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set
y 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))
y9 is Relation-like NAT -defined Function-like V31() [Graph-like] () (y) Subgraph of y
W is Relation-like NAT -defined Function-like V31() [Graph-like] () (y) Subgraph of y
the_Vertices_of y9 is non empty Element of 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
the_Vertices_of W is non empty Element of K32((the_Vertices_of y))
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set
the_Vertices_of G1 is non empty set
y is Relation-like NAT -defined Function-like V31() [Graph-like] set
the_Vertices_of y is non empty set
x is Element of the_Vertices_of G1
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
(G1,x) is non empty Element of K32((the_Vertices_of G1))
y9 is Relation-like NAT -defined Function-like V31() [Graph-like] () (y) Subgraph of y
the_Vertices_of y9 is non empty Element of K32((the_Vertices_of y))
K32((the_Vertices_of y)) is non empty non empty-membered set
W is Element of the_Vertices_of y
(y,W) is non empty Element of K32((the_Vertices_of y))
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set
y is 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))
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
y is Relation-like NAT -defined Function-like V31() [Graph-like] () set
the_Vertices_of y 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
(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
y9 is Element of the_Vertices_of y
{y9} is non empty trivial V31() 1 -element set
(the_Vertices_of y) \ {y9} is Element of K32((the_Vertices_of y))
K32((the_Vertices_of y)) is non empty non empty-membered set
y .edgesBetween ((the_Vertices_of y) \ {y9}) is Element of K32((the_Edges_of y))
the_Edges_of y is set
K32((the_Edges_of y)) is non empty set
(y) is epsilon-transitive epsilon-connected ordinal cardinal set
(y) is non empty Element of K32(K32((the_Vertices_of y)))
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
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 Relation-like NAT -defined Function-like V31() [Graph-like] finite non trivial () set
the_Vertices_of G1 is non empty V31() 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
x is Relation-like NAT -defined Function-like V31() [Graph-like] trivial () set
the_Vertices_of x is non empty V31() set
{G2} is non empty trivial V31() 1 -element set
(the_Vertices_of x) \ {G2} is V31() Element of K32((the_Vertices_of x))
K32((the_Vertices_of x)) is non empty non empty-membered V31() V35() set
x .edgesBetween ((the_Vertices_of x) \ {G2}) is Element of K32((the_Edges_of x))
the_Edges_of x is set
K32((the_Edges_of x)) is non empty set
the Relation-like NAT -defined Function-like V31() [Graph-like] trivial () inducedSubgraph of x,(the_Vertices_of x) \ {G2},x .edgesBetween ((the_Vertices_of x) \ {G2}) is Relation-like NAT -defined Function-like V31() [Graph-like] trivial () inducedSubgraph of x,(the_Vertices_of x) \ {G2},x .edgesBetween ((the_Vertices_of x) \ {G2})
(x) is epsilon-transitive epsilon-connected ordinal cardinal set
(x) is non empty V31() V35() Element of K32(K32((the_Vertices_of x)))
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
( the Relation-like NAT -defined Function-like V31() [Graph-like] trivial () inducedSubgraph of x,(the_Vertices_of x) \ {G2},x .edgesBetween ((the_Vertices_of x) \ {G2})) is epsilon-transitive epsilon-connected ordinal cardinal set
( the Relation-like NAT -defined Function-like V31() [Graph-like] trivial () inducedSubgraph of x,(the_Vertices_of x) \ {G2},x .edgesBetween ((the_Vertices_of x) \ {G2})) is non empty V31() V35() Element of K32(K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] trivial () inducedSubgraph of x,(the_Vertices_of x) \ {G2},x .edgesBetween ((the_Vertices_of x) \ {G2}))))
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] trivial () inducedSubgraph of x,(the_Vertices_of x) \ {G2},x .edgesBetween ((the_Vertices_of x) \ {G2}) is non empty V31() set
K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] trivial () inducedSubgraph of x,(the_Vertices_of x) \ {G2},x .edgesBetween ((the_Vertices_of x) \ {G2}))) is non empty non empty-membered V31() V35() set
K32(K32((the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] trivial () inducedSubgraph of x,(the_Vertices_of x) \ {G2},x .edgesBetween ((the_Vertices_of x) \ {G2})))) is non empty non empty-membered V31() V35() set
card ( the Relation-like NAT -defined Function-like V31() [Graph-like] trivial () inducedSubgraph of x,(the_Vertices_of x) \ {G2},x .edgesBetween ((the_Vertices_of x) \ {G2})) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real set
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
y is Element of the_Vertices_of G2
{y} is non empty trivial V31() 1 -element set
(the_Vertices_of G2) \ {y} is Element of K32((the_Vertices_of G2))
K32((the_Vertices_of G2)) is non empty non empty-membered set
G2 .edgesBetween ((the_Vertices_of G2) \ {y}) is Element of K32((the_Edges_of G2))
the_Edges_of G2 is set
K32((the_Edges_of G2)) is non empty set
(G2) is epsilon-transitive epsilon-connected ordinal cardinal set
(G2) is non empty Element of K32(K32((the_Vertices_of G2)))
K32(K32((the_Vertices_of G2))) is non empty non empty-membered set
card (G2) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
y9 is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G2,(the_Vertices_of G2) \ {y},G2 .edgesBetween ((the_Vertices_of G2) \ {y})
(y9) is epsilon-transitive epsilon-connected ordinal cardinal set
(y9) is non empty Element of K32(K32((the_Vertices_of y9)))
the_Vertices_of y9 is non empty set
K32((the_Vertices_of y9)) is non empty non empty-membered set
K32(K32((the_Vertices_of y9))) is non empty non empty-membered set
card (y9) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
{x} is non empty trivial V31() 1 -element set
(the_Vertices_of G1) \ {x} 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) \ {x}) 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] inducedSubgraph of G1,(the_Vertices_of G1) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x}) is Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x})
(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
( the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x})) 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) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x})) 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) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x}))))
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x}) 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) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x}))) 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) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x})))) 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) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x})) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
the_Vertices_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x}) is non empty Element of K32((the_Vertices_of G1))
{y} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of G2))
(the_Vertices_of G1) \ {y} is Element of K32((the_Vertices_of G1))
(the_Vertices_of G2) \ {y} is Element of K32((the_Vertices_of G2))
the_Vertices_of y9 is non empty Element of K32((the_Vertices_of G2))
the_Edges_of the Relation-like NAT -defined Function-like V31() [Graph-like] inducedSubgraph of G1,(the_Vertices_of G1) \ {x},G1 .edgesBetween ((the_Vertices_of G1) \ {x}) is Element of K32((the_Edges_of G1))
{x} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of G1))
(the_Vertices_of G1) \ {x} is Element of K32((the_Vertices_of G1))
G1 .edgesBetween ((the_Vertices_of G1) \ {x}) is Element of K32((the_Edges_of G1))
G1 .edgesBetween ((the_Vertices_of G2) \ {y}) is Element of K32((the_Edges_of G1))
G2 .edgesBetween ((the_Vertices_of G2) \ {y}) is Element of K32((the_Edges_of G2))
the_Edges_of y9 is Element of K32((the_Edges_of G2))
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite () set
G1 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G1 .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G1 .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 is non empty 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 set
x .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
y is Relation-like NAT -defined Function-like V31() [Graph-like] finite non trivial () set
the_Vertices_of y is non empty V31() set
y9 is Element of the_Vertices_of y
W is Element of the_Vertices_of y
{y9} is non empty trivial V31() 1 -element set
(the_Vertices_of y) \ {y9} is V31() Element of K32((the_Vertices_of y))
K32((the_Vertices_of y)) is non empty non empty-membered V31() V35() set
y .edgesBetween ((the_Vertices_of y) \ {y9}) is V31() Element of K32((the_Edges_of y))
the_Edges_of y is V31() set
K32((the_Edges_of y)) is non empty V31() V35() set
the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of y,(the_Vertices_of y) \ {y9},y .edgesBetween ((the_Vertices_of y) \ {y9}) is Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of y,(the_Vertices_of y) \ {y9},y .edgesBetween ((the_Vertices_of y) \ {y9})
the Relation-like NAT -defined Function-like V31() [Graph-like] finite inducedSubgraph of y,(the_Vertices_of y) \ {y9},y .edgesBetween ((the_Vertices_of y) \ {y9}) .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 y,(the_Vertices_of y) \ {y9},y .edgesBetween ((the_Vertices_of y) \ {y9}) .order()) + 1 is 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 y,(the_Vertices_of y) \ {y9},y .edgesBetween ((the_Vertices_of y) \ {y9}) .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
y9 .edgesInOut() is V31() Element of K32((the_Edges_of y))
card (y9 .edgesInOut()) is 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 y,(the_Vertices_of y) \ {y9},y .edgesBetween ((the_Vertices_of y) \ {y9}) .size()) + (card (y9 .edgesInOut())) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
x .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(x .size()) - (card (y9 .edgesInOut())) is V46() V47() V95() ext-real set
((x .size()) - (card (y9 .edgesInOut()))) + 1 is V46() V47() V95() ext-real set
(x .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
((x .size()) + 1) - (card (y9 .edgesInOut())) is V46() V47() V95() ext-real set
(((x .size()) + 1) - (card (y9 .edgesInOut()))) + (card (y9 .edgesInOut())) is V46() V47() V95() ext-real set
G2 is Relation-like NAT -defined Function-like V31() [Graph-like] finite set
G2 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G2 .size()) + 1 is 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] loopless non-multi non-Dmulti simple Dsimple () set
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] loopless non-multi non-Dmulti simple Dsimple () set
x is set
G2 is Relation-like Function-like FinSequence-like Trail-like Path-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
G2 .last() is Element of the_Vertices_of G1
the_Vertices_of G1 is non empty set
(G2 .last()) .edgesInOut() is Element of K32((the_Edges_of G1))
G2 .addEdge x is Relation-like Function-like FinSequence-like Walk of G1
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non trivial non-multi non-Dmulti simple Dsimple () set
the_Edges_of G1 is V31() set
the_Vertices_of G1 is non empty V31() set
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] set
G2 is Relation-like NAT -defined Function-like V31() [Graph-like] set
x is Relation-like NAT -defined Function-like V31() [Graph-like] loopless non-multi non-Dmulti simple Dsimple () set
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non trivial non-multi non-Dmulti simple Dsimple () () () set
the_Vertices_of G1 is non empty V31() set
G1 is Relation-like NAT -defined Function-like V31() [Graph-like] finite set
G1 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G1 .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G1 .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set
the_Vertices_of G2 is non empty V31() set
the_Edges_of G2 is V31() set
G2 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
card (the_Vertices_of G2) is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
y9 is set
{y9} is non empty trivial V31() 1 -element set
W9 is set
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) V31() Element of K32(K33((the_Edges_of G2),(the_Vertices_of G2)))
K33((the_Edges_of G2),(the_Vertices_of G2)) is Relation-like V31() set
K32(K33((the_Edges_of G2),(the_Vertices_of G2))) is non empty V31() V35() set
(the_Target_of G2) . W9 is set
W is Element of the_Vertices_of G2
{W} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of G2))
K32((the_Vertices_of G2)) is non empty non empty-membered V31() V35() set
the_Source_of G2 is Relation-like Function-like V27( the_Edges_of G2) V28( the_Edges_of G2, the_Vertices_of G2) V31() Element of K32(K33((the_Edges_of G2),(the_Vertices_of G2)))
(the_Source_of G2) . W9 is set
G2 .walkOf (W,W9,W) is Relation-like Function-like FinSequence-like closed Trail-like Path-like Walk of G2
card (the_Edges_of G2) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G2 .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () set
G2 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G2 .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 is non empty 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 loopless non-multi non-Dmulti simple Dsimple () () () set
x .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
y is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non trivial non-multi non-Dmulti simple Dsimple () () () set
the_Vertices_of y is non empty V31() set
the endvertex Element of the_Vertices_of y is endvertex Element of the_Vertices_of y
{ the endvertex Element of the_Vertices_of y} is non empty trivial V31() 1 -element set
(the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y} is V31() Element of K32((the_Vertices_of y))
K32((the_Vertices_of y)) is non empty non empty-membered V31() V35() set
y .edgesBetween ((the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y}) is V31() Element of K32((the_Edges_of y))
the_Edges_of y is V31() set
K32((the_Edges_of y)) is non empty V31() V35() set
the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () inducedSubgraph of y,(the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y},y .edgesBetween ((the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y}) is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () inducedSubgraph of y,(the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y},y .edgesBetween ((the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y})
the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () inducedSubgraph of y,(the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y},y .edgesBetween ((the_Vertices_of y) \ { the endvertex Element of the_Vertices_of 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 loopless non-multi non-Dmulti simple Dsimple () () () inducedSubgraph of y,(the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y},y .edgesBetween ((the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y}) .order()) + 1 is 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 loopless non-multi non-Dmulti simple Dsimple () () () inducedSubgraph of y,(the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y},y .edgesBetween ((the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y}) .order()) + 1) - 1 is V46() V47() V95() ext-real set
(G2 + 1) - 1 is V46() V47() V95() ext-real set
the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () () () inducedSubgraph of y,(the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y},y .edgesBetween ((the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y}) .size() is 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 loopless non-multi non-Dmulti simple Dsimple () () () inducedSubgraph of y,(the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y},y .edgesBetween ((the_Vertices_of y) \ { the endvertex Element of the_Vertices_of y}) .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
the endvertex Element of the_Vertices_of y .edgesInOut() is V31() Element of K32((the_Edges_of y))
card ( the endvertex Element of the_Vertices_of y .edgesInOut()) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
the endvertex Element of the_Vertices_of y .degree() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
x .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(x .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 is non empty 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 loopless non-multi non-Dmulti simple Dsimple () () () set
x .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
x .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(x .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 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 loopless non-multi non-Dmulti simple Dsimple () set
x .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
x .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(x .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
the_Edges_of x is V31() set
y is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non trivial non-multi non-Dmulti simple Dsimple () set
the_Vertices_of y is non empty V31() set
y9 is Element of the_Vertices_of y
W is Element of the_Vertices_of y
(y,y9) is non empty V31() Element of K32((the_Vertices_of y))
K32((the_Vertices_of y)) is non empty non empty-membered V31() V35() set
the_Vertices_of x is non empty V31() set
{y9} is non empty trivial V31() 1 -element set
(the_Vertices_of x) \ {y9} is V31() Element of K32((the_Vertices_of x))
K32((the_Vertices_of x)) is non empty non empty-membered V31() V35() set
x .edgesBetween ((the_Vertices_of x) \ {y9}) is V31() Element of K32((the_Edges_of x))
K32((the_Edges_of x)) is non empty V31() V35() set
the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () inducedSubgraph of x,(the_Vertices_of x) \ {y9},x .edgesBetween ((the_Vertices_of x) \ {y9}) is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () inducedSubgraph of x,(the_Vertices_of x) \ {y9},x .edgesBetween ((the_Vertices_of x) \ {y9})
the Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () inducedSubgraph of x,(the_Vertices_of x) \ {y9},x .edgesBetween ((the_Vertices_of x) \ {y9}) .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 loopless non-multi non-Dmulti simple Dsimple () inducedSubgraph of x,(the_Vertices_of x) \ {y9},x .edgesBetween ((the_Vertices_of x) \ {y9}) .order()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
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 loopless non-multi non-Dmulti simple Dsimple () inducedSubgraph of x,(the_Vertices_of x) \ {y9},x .edgesBetween ((the_Vertices_of x) \ {y9}) .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
y9 .edgesInOut() is V31() Element of K32((the_Edges_of y))
the_Edges_of y is V31() set
K32((the_Edges_of y)) is non empty V31() V35() set
card (y9 .edgesInOut()) is 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 loopless non-multi non-Dmulti simple Dsimple () inducedSubgraph of x,(the_Vertices_of x) \ {y9},x .edgesBetween ((the_Vertices_of x) \ {y9}) .size()) + (card (y9 .edgesInOut())) is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
y .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
y9 .degree() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
W9 is set
{W9} is non empty trivial V31() 1 -element set
G2 is non empty 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 loopless non-multi non-Dmulti simple Dsimple () set
x .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
x .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(x .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () set
G2 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G2 .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
the_Vertices_of G2 is non empty V31() set
x is Element of the_Vertices_of G2
{x} is non empty trivial V31() 1 -element Element of K32((the_Vertices_of G2))
K32((the_Vertices_of G2)) is non empty non empty-membered V31() V35() set
y is Element of the_Vertices_of G2
y9 is Element of the_Vertices_of G2
G2 .walkOf x is Relation-like Function-like FinSequence-like closed directed trivial Trail-like Path-like vertex-distinct Walk of G2
G2 is Relation-like NAT -defined Function-like V31() [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple () set
G2 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G2 .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G2 .size()) + 1 is 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] finite set
G1 .order() is non empty epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
G1 .size() is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
(G1 .size()) + 1 is epsilon-transitive epsilon-connected ordinal natural V31() cardinal V46() V47() V95() ext-real Element of NAT
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 V31() set
K32((the_Edges_of G1)) is non empty V31() V35() set
choose (G2 .edges()) is Element of G2 .edges()
the_Vertices_of G1 is non empty V31() set
{(choose (G2 .edges()))} is non empty trivial V31() 1 -element set
(the_Edges_of G1) \ {(choose (G2 .edges()))} is V31() Element of K32((the_Edges_of G1))
the Relation-like NAT -defined Function-like V31() [Graph-like] finite spanning inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ {(choose (G2 .edges()))} is Relation-like NAT -defined Function-like V31() [Graph-like] finite spanning inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ {(choose (G2 .edges()))}
the Relation-like NAT -defined Function-like V31() [Graph-like] finite spanning inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ {(choose (G2 .edges()))} .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 spanning inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ {(choose (G2 .edges()))} .size() is 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 spanning inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ {(choose (G2 .edges()))} .size()) + 1 is 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 spanning inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ {(choose (G2 .edges()))} .size()) + 1) + 1 is 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 spanning inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ {(choose (G2 .edges()))} .size()) + 1) + 0 is 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
G2 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 set
the Element of the_Vertices_of G1 is Element of the_Vertices_of G1
y is Relation-like Function-like FinSequence-like directed 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] set
x is set
the_Vertices_of G2 is non empty set
the_Vertices_of G1 is non empty set
y is Element of the_Vertices_of G2
y9 is Element of the_Vertices_of G1
W is Relation-like Function-like FinSequence-like directed Walk of G1
W9 is Relation-like Function-like FinSequence-like directed Walk of G2
W9 is Relation-like Function-like FinSequence-like directed Walk of G2