let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for W being Walk of G2 holds W is Walk of G1
let G2 be Subgraph of G1; :: thesis: for W being Walk of G2 holds W is Walk of G1
let W be Walk of G2; :: thesis: W is Walk of G1
set VG1 = the_Vertices_of G1;
set VG2 = the_Vertices_of G2;
set EG1 = the_Edges_of G1;
set EG2 = the_Edges_of G2;
( the_Vertices_of G2 c= (the_Vertices_of G1) \/ (the_Edges_of G1) & the_Edges_of G2 c= (the_Vertices_of G1) \/ (the_Edges_of G1) ) by XBOOLE_1:10;
then (the_Vertices_of G2) \/ (the_Edges_of G2) c= (the_Vertices_of G1) \/ (the_Edges_of G1) by XBOOLE_1:8;
then for y being set st y in rng W holds
y in (the_Vertices_of G1) \/ (the_Edges_of G1) by TARSKI:def 3;
then rng W c= (the_Vertices_of G1) \/ (the_Edges_of G1) by TARSKI:def 3;
then A1: W is FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1) by FINSEQ_1:def 4;

now

thus not len W is even ; :: thesis: ( W . 1 in the_Vertices_of G1 & ( for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G1 ) )
W . 1 in the_Vertices_of G2 by Def3;
hence W . 1 in the_Vertices_of G1 ; :: thesis: for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G1
let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G1 )
assume n < len W ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G1
then W . (n + 1) Joins W . n,W . (n + 2),G2 by Def3;
hence W . (n + 1) Joins W . n,W . (n + 2),G1 by GLIB_000:75; :: thesis: verum

end;

hence W is Walk of G1 by A1, Def3; :: thesis: verum