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

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 G2end;

hence
W is Walk of G2
; :: thesis: verumper cases
( not W is trivial or W is trivial )
;

end;