let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for W being Walk of G2 holds
( ( W is closed implies W is closed Walk of G1 ) & ( W is directed implies W is directed Walk of G1 ) & ( W is trivial implies W is trivial Walk of G1 ) & ( W is Trail-like implies W is Trail-like Walk of G1 ) & ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )
let G2 be Subgraph of G1; :: thesis: for W being Walk of G2 holds
( ( W is closed implies W is closed Walk of G1 ) & ( W is directed implies W is directed Walk of G1 ) & ( W is trivial implies W is trivial Walk of G1 ) & ( W is Trail-like implies W is Trail-like Walk of G1 ) & ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )
let W be Walk of G2; :: thesis: ( ( W is closed implies W is closed Walk of G1 ) & ( W is directed implies W is directed Walk of G1 ) & ( W is trivial implies W is trivial Walk of G1 ) & ( W is Trail-like implies W is Trail-like Walk of G1 ) & ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )
reconsider W' = W as Walk of G1 by Th168;

hereby :: thesis: ( ( W is directed implies W is directed Walk of G1 ) & ( W is trivial implies W is trivial Walk of G1 ) & ( W is Trail-like implies W is Trail-like Walk of G1 ) & ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )

assume W is closed ; :: thesis: W is closed Walk of G1
then W .first() = W .last() by Def24;
then W' .first() = W' .last() ;
hence W is closed Walk of G1 by Def24; :: thesis: verum

end;

hereby :: thesis: ( ( W is trivial implies W is trivial Walk of G1 ) & ( W is Trail-like implies W is Trail-like Walk of G1 ) & ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )

assume A1: W is directed ; :: thesis: W is directed Walk of G1

now

let n be odd Element of NAT ; :: thesis: ( n < len W' implies (the_Source_of G1) . (W' . (n + 1)) = W' . n )
assume A2: n < len W' ; :: thesis: (the_Source_of G1) . (W' . (n + 1)) = W' . n
then A3: (the_Source_of G2) . (W' . (n + 1)) = W' . n by A1, Def25;
A4: 1 <= n + 1 by NAT_1:12;
n + 1 <= len W' by A2, NAT_1:13;
then n + 1 in dom W' by A4, FINSEQ_3:27;
then W' . (n + 1) in the_Edges_of G2 by Th9;
hence (the_Source_of G1) . (W' . (n + 1)) = W' . n by A3, GLIB_000:def 34; :: thesis: verum

end;

hence W is directed Walk of G1 by Def25; :: thesis: verum

end;

hereby :: thesis: ( ( W is Trail-like implies W is Trail-like Walk of G1 ) & ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )

assume W is trivial ; :: thesis: W is trivial Walk of G1
then len W' = 1 by Lm55;
hence W is trivial Walk of G1 by Lm54; :: thesis: verum

end;

A5: now

assume W is Trail-like ; :: thesis: W is Trail-like Walk of G1
then for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W' . m <> W' . n by Lm57;
hence W is Trail-like Walk of G1 by Lm57; :: thesis: verum

end;

hence ( W is Trail-like implies W is Trail-like Walk of G1 ) ; :: thesis: ( ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )

now

assume W is Path-like ; :: thesis: W is Path-like Walk of G1
then ( W' is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len W' & W' . m = W' . n holds
( m = 1 & n = len W' ) ) ) by A5, Def28;
hence W is Path-like Walk of G1 by Def28; :: thesis: verum

end;

hence ( W is Path-like implies W is Path-like Walk of G1 ) ; :: thesis: ( W is vertex-distinct implies W is vertex-distinct Walk of G1 )

hereby :: thesis: verum

assume W is vertex-distinct ; :: thesis: W is vertex-distinct Walk of G1
then for m, n being odd Element of NAT st m <= len W' & n <= len W' & W' . m = W' . n holds
m = n by Def29;
hence W is vertex-distinct Walk of G1 by Def29; :: thesis: verum

end;

thus verum ; :: thesis: verum