let G1 be _Graph; :: thesis:
let G2 be Subgraph of G1; :: thesis:
let W be Walk of G1; :: thesis:
assume that
A1: W is V5() and
A2: W .edges() c= the_Edges_of G2 ; :: thesis:
set VG2 = the_Vertices_of G2;
set EG2 = the_Edges_of G2;
set WV = W .vertices() ;
set WE = W .edges() ;

A3: now :: thesis:

let n be odd Element of NAT ; :: thesis:
assume A4: n <= len W ; :: thesis:

now :: thesis:

per cases ;

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

A6: 1 <= n by ABIAN:12;
n <> 1 by A1, A5, Lm54;
then 1 < n by A6, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then reconsider n5 = n - (2 * 1) as odd Element of NAT by INT_1:5;
n5 + 1 = n - (2 - 1) ;
then A7: n5 + 1 <= (len W) - 0 by A5, XREAL_1:13;
n5 < (len W) - 0 by A5, XREAL_1:15;
then A8: W . (n5 + 1) Joins W . n5,W . (n5 + 2),G1 by Def3;
1 <= n5 + 1 by NAT_1:12;
then W . (n5 + 1) in W .edges() by A7, Lm46;
then W . (n5 + 1) Joins W . n5,W . (n5 + 2),G2 by A2, A8, GLIB_000:73;
hence W . n in the_Vertices_of G2 by GLIB_000:13; :: thesis:

end;

suppose n <> len W ; :: thesis:

then A9: n < len W by A4, XXREAL_0:1;
then A10: W . (n + 1) Joins W . n,W . (n + 2),G1 by Def3;
A11: 1 <= n + 1 by NAT_1:12;
n + 1 <= len W by A9, NAT_1:13;
then W . (n + 1) in W .edges() by A11, Lm46;
then W . (n + 1) Joins W . n,W . (n + 2),G2 by A2, A10, GLIB_000:73;
hence W . n in the_Vertices_of G2 by GLIB_000:13; :: thesis:

end;

end;

end;

hence W . n in the_Vertices_of G2 ; :: thesis:

end;

now :: thesis:

let y be object ; :: thesis:
assume y in rng W ; :: thesis:
then A12: y in (W .vertices()) \/ (W .edges()) by Th99;

now :: thesis:

per cases by A12, XBOOLE_0:def 3;

suppose y in W .vertices() ; :: thesis:

then ex n being odd Element of NAT st
( n <= len W & W . n = y ) by Lm45;
then y in the_Vertices_of G2 by A3;
hence y in (the_Vertices_of G2) \/ (the_Edges_of G2) by XBOOLE_0:def 3; :: thesis:

end;

suppose y in W .edges() ; :: thesis:

hence y in (the_Vertices_of G2) \/ (the_Edges_of G2) by A2, XBOOLE_0:def 3; :: thesis:

end;

end;

end;

hence y in (the_Vertices_of G2) \/ (the_Edges_of G2) ; :: thesis:

end;

then rng W c= (the_Vertices_of G2) \/ (the_Edges_of G2) by TARSKI:def 3;
then A13: W is FinSequence of (the_Vertices_of G2) \/ (the_Edges_of G2) by FINSEQ_1:def 4;

now :: thesis:

reconsider aa1 = 1 as odd Element of NAT by JORDAN12:2;
thus len W is odd ; :: thesis:
aa1 <= len W by ABIAN:12;
hence W . 1 in the_Vertices_of G2 by A3; :: thesis:
let n be odd Element of NAT ; :: thesis:
A14: 1 <= n + 1 by NAT_1:12;
assume A15: n < len W ; :: thesis:
then A16: W . (n + 1) Joins W . n,W . (n + 2),G1 by Def3;
n + 1 <= len W by A15, NAT_1:13;
then W . (n + 1) in W .edges() by A14, Lm46;
hence W . (n + 1) Joins W . n,W . (n + 2),G2 by A2, A16, GLIB_000:73; :: thesis:

end;

hence W is Walk of G2 by A13, Def3; :: thesis: