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