let G be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for W2 being Walk of G2 holds W2 is Walk of G1
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for W2 being Walk of G2 holds W2 is Walk of G1
let V be set ; :: thesis: for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for W2 being Walk of G2 holds W2 is Walk of G1
let G1 be addAdjVertexToAll of G,v,V; :: thesis: for G2 being addAdjVertexFromAll of G,v,V
for W2 being Walk of G2 holds W2 is Walk of G1
let G2 be addAdjVertexFromAll of G,v,V; :: thesis: for W2 being Walk of G2 holds W2 is Walk of G1
let W2 be Walk of G2; :: thesis: W2 is Walk of G1

per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;

suppose ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: W2 is Walk of G1

then G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} by Th35;
hence W2 is Walk of G1 by Th14; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: W2 is Walk of G1

then ( G1 == G & G2 == G ) by Def2, Def3;
hence W2 is Walk of G1 by GLIB_000:85, GLIB_001:179; :: thesis: verum

end;

end;