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 V5() or not W is V5() ) ;
suppose W is V5() ; :: thesis: W is Walk of G2
hence W is Walk of G2 by A2, Th167; :: thesis: verum
end;
end;
end;
hence W is Walk of G2 ; :: thesis: verum