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 W9 = W as Walk of G1 by Th165;

( W is Path-like implies W is Path-like Walk of G1 ) by A5, Def28;

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 )

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 W9 = W as Walk of G1 by Th165;

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() ;

then W9 .first() = W9 .last() ;

hence W is closed Walk of G1 by Def24; :: thesis: verum

end;then W .first() = W .last() ;

then W9 .first() = W9 .last() ;

hence W is closed Walk of G1 by Def24; :: thesis: verum

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

end;now :: thesis: for n being odd Element of NAT st n < len W9 holds

(the_Source_of G1) . (W9 . (n + 1)) = W9 . n

hence
W is directed Walk of G1
by Def25; :: thesis: verum(the_Source_of G1) . (W9 . (n + 1)) = W9 . n

let n be odd Element of NAT ; :: thesis: ( n < len W9 implies (the_Source_of G1) . (W9 . (n + 1)) = W9 . n )

A2: 1 <= n + 1 by NAT_1:12;

assume A3: n < len W9 ; :: thesis: (the_Source_of G1) . (W9 . (n + 1)) = W9 . n

then n + 1 <= len W9 by NAT_1:13;

then n + 1 in dom W9 by A2, FINSEQ_3:25;

then A4: W9 . (n + 1) in the_Edges_of G2 by Th7;

(the_Source_of G2) . (W9 . (n + 1)) = W9 . n by A1, A3;

hence (the_Source_of G1) . (W9 . (n + 1)) = W9 . n by A4, GLIB_000:def 32; :: thesis: verum

end;A2: 1 <= n + 1 by NAT_1:12;

assume A3: n < len W9 ; :: thesis: (the_Source_of G1) . (W9 . (n + 1)) = W9 . n

then n + 1 <= len W9 by NAT_1:13;

then n + 1 in dom W9 by A2, FINSEQ_3:25;

then A4: W9 . (n + 1) in the_Edges_of G2 by Th7;

(the_Source_of G2) . (W9 . (n + 1)) = W9 . n by A1, A3;

hence (the_Source_of G1) . (W9 . (n + 1)) = W9 . n by A4, GLIB_000:def 32; :: thesis: verum

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 W9 = 1 by Lm55;

hence W is trivial Walk of G1 by Lm54; :: thesis: verum

end;then len W9 = 1 by Lm55;

hence W is trivial Walk of G1 by Lm54; :: thesis: verum

A5: now :: thesis: ( W is Trail-like implies W is Trail-like Walk of G1 )

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 ) )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

W9 . m <> W9 . n by Lm57;

hence W is Trail-like Walk of G1 by Lm57; :: thesis: verum

end;then for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W9 . m <> W9 . n by Lm57;

hence W is Trail-like Walk of G1 by Lm57; :: thesis: verum

( W is Path-like implies W is Path-like Walk of G1 ) by A5, Def28;

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 W9 & n <= len W9 & W9 . m = W9 . n holds

m = n ;

hence W is vertex-distinct Walk of G1 by Def29; :: thesis: verum

end;then for m, n being odd Element of NAT st m <= len W9 & n <= len W9 & W9 . m = W9 . n holds

m = n ;

hence W is vertex-distinct Walk of G1 by Def29; :: thesis: verum