let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
let W be Walk of G1; :: thesis:
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis:
consider E being set such that
A2: ( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
A3: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by A1, Def4;
A4: E /\ (the_Edges_of G2) = {} by A2, XBOOLE_0:def 7;

hereby :: thesis:

assume A5: ( W .edges() c= the_Edges_of G2 & W is trivial ) ; :: thesis:
thus not v in W .vertices() :: thesis:

assume v in W .vertices() ; :: thesis:
then consider n being odd Element of NAT such that
A6: ( n <= len W & W . n = v ) by GLIB_001:87;

per cases by A6, XXREAL_0:1;

suppose A7: n = len W ; :: thesis:

A8: 1 <> len W by A5, GLIB_001:126;
1 <= len W by ABIAN:12;
then 1 < len W by A8, XXREAL_0:1;
then reconsider m = (len W) - 2 as odd Element of NAT by Lm13;
A9: m < (len W) - 0 by XREAL_1:15;
then W . (m + 1) Joins W . m,W . (m + 2),G1 by GLIB_001:def 3;
then A10: W . (m + 1) Joins W . m,v,G1 by A6, A7;
then W . m in V by A1, Def4;
then consider e1 being object such that
A11: ( e1 in E & e1 Joins W . m,v,G1 ) and
A12: for e2 being object st e2 Joins W . m,v,G1 holds
e1 = e2 by A3;
W . (m + 1) in E by A10, A11, A12;
then not W . (m + 1) in W .edges() by A5, A4, Lm7;
hence contradiction by A9, GLIB_001:100; :: thesis:

end;

suppose A13: n < len W ; :: thesis:

then A14: W . (n + 1) Joins W . (n + 2),v,G1 by A6, GLIB_000:14, GLIB_001:def 3;
then W . (n + 2) in V by A1, Def4;
then consider e1 being object such that
A15: ( e1 in E & e1 Joins W . (n + 2),v,G1 ) and
A16: for e2 being object st e2 Joins W . (n + 2),v,G1 holds
e1 = e2 by A3;
W . (n + 1) in E by A14, A15, A16;
then not W . (n + 1) in W .edges() by A5, A4, Lm7;
hence contradiction by A13, GLIB_001:100; :: thesis:

end;

end;

end;

end;

assume A17: not v in W .vertices() ; :: thesis:
for e being object st e in W .edges() holds
e in the_Edges_of G2

let e be object ; :: thesis:
assume e in W .edges() ; :: thesis:
then consider n being odd Element of NAT such that
A18: ( n < len W & W . (n + 1) = e ) by GLIB_001:100;
A19: e Joins W . n,W . (n + 2),G1 by A18, GLIB_001:def 3;
( W . n <> v & W . (n + 2) <> v )

thus W . n <> v by A17, A18, GLIB_001:87; :: thesis:
A20: n + 2 <= len W by A18, GLIB_001:1;
assume W . (n + 2) = v ; :: thesis:
hence contradiction by A17, A20, GLIB_001:87; :: thesis:

end;

then e Joins W . n,W . (n + 2),G2 by A19, A1, Th49;
hence e in the_Edges_of G2 by GLIB_000:def 13; :: thesis:

end;

hence W .edges() c= the_Edges_of G2 by TARSKI:def 3; :: thesis: