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 V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( ( W .edges() c= the_Edges_of G2 & W is trivial ) or not v in W .vertices() ) holds
W is Walk 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 V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( ( W .edges() c= the_Edges_of G2 & W is trivial ) or not v in W .vertices() ) holds
W is Walk of G2
let V be set ; :: thesis: for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( ( W .edges() c= the_Edges_of G2 & W is trivial ) or not v in W .vertices() ) holds
W is Walk of G2
let G1 be addAdjVertexAll of G2,v,V; :: thesis: for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( ( W .edges() c= the_Edges_of G2 & W is trivial ) or not v in W .vertices() ) holds
W is Walk of G2
let W be Walk of G1; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( ( W .edges() c= the_Edges_of G2 & W is trivial ) or not v in W .vertices() ) implies W is Walk of G2 )
assume that
A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: ( ( W .edges() c= the_Edges_of G2 & W is trivial ) or not v in W .vertices() ) ; :: thesis: W is Walk of G2
A3: ( W .edges() c= the_Edges_of G2 & not v in W .vertices() ) by A1, A2, Th63;
for w being object st w in W .vertices() holds
w in the_Vertices_of G2

proof

let w be object ; :: thesis: ( w in W .vertices() implies w in the_Vertices_of G2 )
assume A4: w in W .vertices() ; :: thesis: w in the_Vertices_of G2
then A5: w in the_Vertices_of G1 ;
assume A6: not w in the_Vertices_of G2 ; :: thesis: contradiction
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A1, Def4;
then w in {v} by A5, A6, XBOOLE_0:def 3;
hence contradiction by A4, A3, TARSKI:def 1; :: thesis: verum

end;

then A7: W .vertices() c= the_Vertices_of G2 by TARSKI:def 3;
rng W = (W .vertices()) \/ (W .edges()) by GLIB_001:101;
then A8: W is FinSequence of (the_Vertices_of G2) \/ (the_Edges_of G2) by FINSEQ_1:def 4, A7, A3, XBOOLE_1:13;

now :: thesis: ( len W is odd & W . 1 in the_Vertices_of G2 & ( for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G2 ) )

thus len W is odd ; :: thesis: ( W . 1 in the_Vertices_of G2 & ( for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G2 ) )
W .first() in W .vertices() by GLIB_001:88;
then W . 1 in W .vertices() by GLIB_001:def 6;
hence W . 1 in the_Vertices_of G2 by A7; :: thesis: for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G2
let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G2 )
assume A9: n < len W ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G2
then A10: W . (n + 1) Joins W . n,W . (n + 2),G1 by GLIB_001:def 3;
W . (n + 1) in W .edges() by A9, GLIB_001:100;
hence W . (n + 1) Joins W . n,W . (n + 2),G2 by A10, GLIB_006:72, A3; :: thesis: verum

end;

hence W is Walk of G2 by A8, GLIB_001:def 3; :: thesis: verum