let G1 be _Graph; for G2 being Subgraph of G1
for W being Walk of G2 holds W is Walk of G1
let G2 be Subgraph of G1; for W being Walk of G2 holds W is Walk of G1
let W be Walk of G2; 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 ( 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 ) )thus
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 ) )
W . 1
in the_Vertices_of G2
by Def3;
hence
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),G1let n be
odd Element of
NAT ;
( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G1 )assume
n < len W
;
W . (n + 1) Joins W . n,W . (n + 2),G1then
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;
verum end;
the_Vertices_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; verum