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 V5() implies W is V5() 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 V5() implies W is V5() 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 V5() implies W is V5() 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 V5() implies W is V5() 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;
hereby :: thesis: ( ( W is V5() implies W is V5() 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 :: thesis: for n being odd Element of NAT st n < len W9 holds
(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;
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 V5() ; :: thesis: W is V5() Walk of G1
then len W9 = 1 by Lm55;
hence W is V5() Walk of G1 by Lm54; :: thesis: verum
end;
A5: now :: thesis: ( W is Trail-like implies W is Trail-like 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;
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 ) )
( 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;