let G2 be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 holds
W .edges() c= the_Edges_of G2
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 holds
W .edges() c= the_Edges_of G2
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 holds
W .edges() c= the_Edges_of G2
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 holds
W .edges() c= the_Edges_of G2
let W be Walk of G1; :: thesis: ( W .vertices() c= the_Vertices_of G2 implies W .edges() c= the_Edges_of G2 )
assume A1: W .vertices() c= the_Vertices_of G2 ; :: thesis: W .edges() c= the_Edges_of G2

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

suppose A2: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: W .edges() c= the_Edges_of G2

then not v in W .vertices() by A1;
hence W .edges() c= the_Edges_of G2 by A2, Th63; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G2 or v in the_Vertices_of G2 ) ; :: thesis: W .edges() c= the_Edges_of G2

then G1 == G2 by Def4;
then the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
hence W .edges() c= the_Edges_of G2 ; :: thesis: verum

end;

end;