let G1 be _Graph; :: thesis: for G2 being Subgraph of G1

for W being Walk of G1 st W is trivial & W .first() in the_Vertices_of G2 holds

W is Walk of G2

let G2 be Subgraph of G1; :: thesis: for W being Walk of G1 st W is trivial & W .first() in the_Vertices_of G2 holds

W is Walk of G2

let W be Walk of G1; :: thesis: ( W is trivial & W .first() in the_Vertices_of G2 implies W is Walk of G2 )

assume that

A1: W is trivial and

A2: W .first() in the_Vertices_of G2 ; :: thesis: W is Walk of G2

consider v being Vertex of G1 such that

A3: W = G1 .walkOf v by A1, Lm56;

reconsider v9 = v as Vertex of G2 by A2, A3, Th12;

W = G2 .walkOf v9 by A3;

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

for W being Walk of G1 st W is trivial & W .first() in the_Vertices_of G2 holds

W is Walk of G2

let G2 be Subgraph of G1; :: thesis: for W being Walk of G1 st W is trivial & W .first() in the_Vertices_of G2 holds

W is Walk of G2

let W be Walk of G1; :: thesis: ( W is trivial & W .first() in the_Vertices_of G2 implies W is Walk of G2 )

assume that

A1: W is trivial and

A2: W .first() in the_Vertices_of G2 ; :: thesis: W is Walk of G2

consider v being Vertex of G1 such that

A3: W = G1 .walkOf v by A1, Lm56;

reconsider v9 = v as Vertex of G2 by A2, A3, Th12;

W = G2 .walkOf v9 by A3;

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