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;

A1: 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 A1, XBOOLE_1:8;

then for y being object 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 W is FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1) by FINSEQ_1:def 4;

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

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;

A1: the_Edges_of G2 c= (the_Vertices_of G1) \/ (the_Edges_of G1) by XBOOLE_1:10;

A2: now :: thesis: ( len W is odd & 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 ) )

the_Vertices_of G2 c= (the_Vertices_of G1) \/ (the_Edges_of G1)
by XBOOLE_1:10;W . (n + 1) Joins W . n,W . (n + 2),G1 ) )

thus
len W is odd
; :: 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:72; :: thesis: verum

end;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:72; :: thesis: verum

then (the_Vertices_of G2) \/ (the_Edges_of G2) c= (the_Vertices_of G1) \/ (the_Edges_of G1) by A1, XBOOLE_1:8;

then for y being object 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 W is FinSequence of (the_Vertices_of G1) \/ (the_Edges_of G1) by FINSEQ_1:def 4;

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