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

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