let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for W being Walk of G1 st not W is trivial & W .edges() c= the_Edges_of G2 holds
W is Walk of G2

let G2 be Subgraph of G1; :: thesis: for W being Walk of G1 st not W is trivial & W .edges() c= the_Edges_of G2 holds
W is Walk of G2

let W be Walk of G1; :: thesis: ( not W is trivial & W .edges() c= the_Edges_of G2 implies W is Walk of G2 )
assume that
A1: not W is trivial and
A2: W .edges() c= the_Edges_of G2 ; :: thesis: W is Walk of G2
set VG2 = the_Vertices_of G2;
set EG2 = the_Edges_of G2;
set WV = W .vertices() ;
set WE = W .edges() ;
A3: now :: thesis: for n being odd Element of NAT st n <= len W holds
W . n in the_Vertices_of G2
let n be odd Element of NAT ; :: thesis: ( n <= len W implies W . n in the_Vertices_of G2 )
assume A4: n <= len W ; :: thesis:
now :: thesis:
per cases ( n = len W or n <> len W ) ;
suppose A5: n = len W ; :: thesis:
A6: 1 <= n by ABIAN:12;
n <> 1 by A1, A5, Lm54;
then 1 < n by ;
then 1 + 1 <= n by NAT_1:13;
then reconsider n5 = n - (2 * 1) as odd Element of NAT by INT_1:5;
n5 + 1 = n - (2 - 1) ;
then A7: n5 + 1 <= (len W) - 0 by ;
n5 < (len W) - 0 by ;
then A8: W . (n5 + 1) Joins W . n5,W . (n5 + 2),G1 by Def3;
1 <= n5 + 1 by NAT_1:12;
then W . (n5 + 1) in W .edges() by ;
then W . (n5 + 1) Joins W . n5,W . (n5 + 2),G2 by ;
hence W . n in the_Vertices_of G2 by GLIB_000:13; :: thesis: verum
end;
suppose n <> len W ; :: thesis:
then A9: n < len W by ;
then A10: W . (n + 1) Joins W . n,W . (n + 2),G1 by Def3;
A11: 1 <= n + 1 by NAT_1:12;
n + 1 <= len W by ;
then W . (n + 1) in W .edges() by ;
then W . (n + 1) Joins W . n,W . (n + 2),G2 by ;
hence W . n in the_Vertices_of G2 by GLIB_000:13; :: thesis: verum
end;
end;
end;
hence W . n in the_Vertices_of G2 ; :: thesis: verum
end;
now :: thesis: for y being object st y in rng W holds
y in () \/ ()
let y be object ; :: thesis: ( y in rng W implies y in () \/ () )
assume y in rng W ; :: thesis: y in () \/ ()
then A12: y in () \/ () by Th99;
now :: thesis: y in () \/ ()end;
hence y in () \/ () ; :: thesis: verum
end;
then rng W c= () \/ () by TARSKI:def 3;
then A13: W is FinSequence of () \/ () by FINSEQ_1:def 4;
now :: thesis: ( len W is odd & W . 1 in the_Vertices_of G2 & ( for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G2 ) )
reconsider aa1 = 1 as odd Element of NAT by JORDAN12:2;
thus len W is odd ; :: thesis: ( W . 1 in the_Vertices_of G2 & ( for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G2 ) )

aa1 <= len W by ABIAN:12;
hence W . 1 in the_Vertices_of G2 by A3; :: thesis: for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),G2

let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G2 )
A14: 1 <= n + 1 by NAT_1:12;
assume A15: n < len W ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G2
then A16: W . (n + 1) Joins W . n,W . (n + 2),G1 by Def3;
n + 1 <= len W by ;
then W . (n + 1) in W .edges() by ;
hence W . (n + 1) Joins W . n,W . (n + 2),G2 by ; :: thesis: verum
end;
hence W is Walk of G2 by ; :: thesis: verum