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

then A13: W is FinSequence of (the_Vertices_of G2) \/ (the_Edges_of G2) by FINSEQ_1:def 4;

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

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

end;assume A4: n <= len W ; :: thesis: W . n in the_Vertices_of G2

now :: thesis: W . n in the_Vertices_of G2end;

hence
W . n in the_Vertices_of G2
; :: thesis: verumper cases
( n = len W or n <> len W )
;

end;

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

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

now :: thesis: for y being object st y in rng W holds

y in (the_Vertices_of G2) \/ (the_Edges_of G2)

then
rng W c= (the_Vertices_of G2) \/ (the_Edges_of G2)
by TARSKI:def 3;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;

end;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: verumper cases
( y in W .vertices() or y in W .edges() )
by A12, XBOOLE_0:def 3;

end;

suppose
y in W .vertices()
; :: thesis: y in (the_Vertices_of G2) \/ (the_Edges_of G2)

then
ex n being odd Element of NAT st

( n <= len W & W . n = y ) by Lm45;

then y in the_Vertices_of G2 by A3;

hence y in (the_Vertices_of G2) \/ (the_Edges_of G2) by XBOOLE_0:def 3; :: thesis: verum

end;( n <= len W & W . n = y ) by Lm45;

then y in the_Vertices_of G2 by A3;

hence y in (the_Vertices_of G2) \/ (the_Edges_of G2) by XBOOLE_0:def 3; :: thesis: verum

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

hence
W is Walk of G2
by A13, Def3; :: thesis: verumW . (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;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