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;
W = G2 .walkOf v9 by A3;
hence W is Walk of G2 ; :: thesis: verum