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 A1: ( W is trivial & W .first() in the_Vertices_of G2 ) ; :: thesis: W is Walk of G2
then consider v being Vertex of G1 such that
A2: W = G1 .walkOf v by Lm56;
reconsider v' = v as Vertex of G2 by A1, A2, Th14;
W = G2 .walkOf v' by A2;
hence W is Walk of G2 ; :: thesis: verum