let G be _Graph; :: thesis: for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for W being Walk of G st W .vertices() c= S holds
W is Walk of H
let S be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S
for W being Walk of G st W .vertices() c= S holds
W is Walk of H
let H be inducedSubgraph of G,S; :: thesis: for W being Walk of G st W .vertices() c= S holds
W is Walk of H
A1: the_Vertices_of H = S by GLIB_000:def 37;
A2: the_Edges_of H = G .edgesBetween S by GLIB_000:def 37;
let W be Walk of G; :: thesis: ( W .vertices() c= S implies W is Walk of H )
assume W .vertices() c= S ; :: thesis: W is Walk of H
then A3: W .vertices() c= the_Vertices_of H by GLIB_000:def 37;
A4: W .edges() c= G .edgesBetween (W .vertices()) by GLIB_001:109;
G .edgesBetween (W .vertices()) c= G .edgesBetween (the_Vertices_of H) by A3, GLIB_000:36;
then W .edges() c= the_Edges_of H by A1, A2, A4;
hence W is Walk of H by A3, GLIB_001:170; :: thesis: verum