let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for W being Walk of G1 st 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 W is trivial & W .edges() c= the_Edges_of G2 holds
W is Walk of G2
let W be Walk of G1; :: thesis: ( W is trivial & W .edges() c= the_Edges_of G2 implies W is Walk of G2 )
assume that
A1: 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: W . n in the_Vertices_of G2
now :: thesis: W . n in the_Vertices_of G2
per cases ( n = len W or n <> len W ) ;
suppose A5: n = len W ; :: thesis: W . n in the_Vertices_of G2
A6: 1 <= n by ABIAN:12;
n <> 1 by A1, A5, Lm54;
then 1 < n by A6, XXREAL_0:1;
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 A5, XREAL_1:13;
n5 < (len W) - 0 by A5, XREAL_1:15;
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 A7, Lm46;
then W . (n5 + 1) Joins W . n5,W . (n5 + 2),G2 by A2, A8, GLIB_000:73;
hence W . n in the_Vertices_of G2 by GLIB_000:13; :: thesis: verum
end;
suppose n <> len W ; :: thesis: W . n in the_Vertices_of G2
then A9: n < len W by A4, XXREAL_0:1;
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 A9, NAT_1:13;
then W . (n + 1) in W .edges() by A11, Lm46;
then W . (n + 1) Joins W . n,W . (n + 2),G2 by A2, A10, GLIB_000:73;
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 (the_Vertices_of G2) \/ (the_Edges_of G2)
let y be object ; :: thesis: ( y in rng W implies y in (the_Vertices_of G2) \/ (the_Edges_of G2) )
assume y in rng W ; :: thesis: y in (the_Vertices_of G2) \/ (the_Edges_of G2)
then A12: y in (W .vertices()) \/ (W .edges()) by Th99;
now :: thesis: y in (the_Vertices_of G2) \/ (the_Edges_of G2)
end;
hence y in (the_Vertices_of G2) \/ (the_Edges_of G2) ; :: thesis: verum
end;
then rng W c= (the_Vertices_of G2) \/ (the_Edges_of G2) by TARSKI:def 3;
then A13: W is FinSequence of (the_Vertices_of G2) \/ (the_Edges_of G2) 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 A15, NAT_1:13;
then W . (n + 1) in W .edges() by A14, Lm46;
hence W . (n + 1) Joins W . n,W . (n + 2),G2 by A2, A16, GLIB_000:73; :: thesis: verum
end;
hence W is Walk of G2 by A13, Def3; :: thesis: verum