let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 & W .edges() c= the_Edges_of G2 holds
W is Walk of G2
let G2 be Subgraph of G1; :: thesis: for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 & W .edges() c= the_Edges_of G2 holds
W is Walk of G2
let W be Walk of G1; :: thesis: ( W .vertices() c= the_Vertices_of G2 & W .edges() c= the_Edges_of G2 implies W is Walk of G2 )
assume that
A1: W .vertices() c= the_Vertices_of G2 and
A2: W .edges() c= the_Edges_of G2 ; :: thesis: W is Walk of G2

now :: thesis: W is Walk of G2

per cases ( not W is trivial or not W is trivial ) ;

suppose W is trivial ; :: thesis: W is Walk of G2

hence W is Walk of G2 by A2, Th167; :: thesis: verum

end;

suppose A3: W is trivial ; :: thesis: W is Walk of G2

W .first() in W .vertices() by Th86;
hence W is Walk of G2 by A1, A3, Th166; :: thesis: verum

end;

end;

end;

hence W is Walk of G2 ; :: thesis: verum