hereby :: thesis: ( ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W is Walk of G ) & ( for b₁ being Walk of G holds verum ) )

set W2 = (m,n) -cut W;
set VG = the_Vertices_of G;
assume that
A1: m is odd and
A2: n is odd and
A3: m <= n and
A4: n <= len W ; :: thesis: (m,n) -cut W is Walk of G
reconsider m4 = m, n4 = n as odd Nat by A1, A2;
A5: 1 <= m by A1, ABIAN:12;
then ((len ((m,n) -cut W)) + m4) - m4 = (n4 + 1) - m4 by A3, A4, FINSEQ_6:def 4;
then reconsider lenW2 = len ((m,n) -cut W) as odd Element of NAT ;

now :: thesis: ( len ((m,n) -cut W) is odd & ((m,n) -cut W) . 1 in the_Vertices_of G & ( for i being odd Element of NAT st i < len ((m,n) -cut W) holds
((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G ) )

reconsider lenW2aa1 = lenW2 - 1 as Element of NAT by ABIAN:12, INT_1:5;
lenW2 is odd ;
hence len ((m,n) -cut W) is odd ; :: thesis: ( ((m,n) -cut W) . 1 in the_Vertices_of G & ( for i being odd Element of NAT st i < len ((m,n) -cut W) holds
((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G ) )
0 < lenW2aa1 + 1 ;
then A6: ((m,n) -cut W) . (0 + 1) = W . (m + 0) by A3, A4, A5, FINSEQ_6:def 4;
m <= len W by A3, A4, XXREAL_0:2;
then W . m = W .vertexAt m by A1, Def8;
hence ((m,n) -cut W) . 1 in the_Vertices_of G by A6; :: thesis: for i being odd Element of NAT st i < len ((m,n) -cut W) holds
((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G
let i be odd Element of NAT ; :: thesis: ( i < len ((m,n) -cut W) implies ((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G )
reconsider x = (m4 + i) - 1 as odd Element of NAT by A5, INT_1:5, NAT_1:12;
reconsider iaa1 = i - 1 as even Element of NAT by ABIAN:12, INT_1:5;
assume A7: i < len ((m,n) -cut W) ; :: thesis: ((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G
then i + 1 <= lenW2 by NAT_1:13;
then i + 1 < len ((m,n) -cut W) by XXREAL_0:1;
then A8: ((m,n) -cut W) . ((i + 1) + 1) = W . (m + (i + 1)) by A3, A4, A5, FINSEQ_6:def 4;
i + m < (len ((m,n) -cut W)) + m by A7, XREAL_1:8;
then i + m < n + 1 by A3, A4, A5, FINSEQ_6:def 4;
then i + m4 <= n4 by NAT_1:13;
then m4 + i < n4 by XXREAL_0:1;
then m + i < len W by A4, XXREAL_0:2;
then (m + i) - 1 < (len W) - 0 by XREAL_1:14;
then A9: W . (x + 1) Joins W . x,W . (x + 2),G by Def3;
iaa1 < (len ((m,n) -cut W)) - 0 by A7, XREAL_1:14;
then ((m,n) -cut W) . (iaa1 + 1) = W . (m + iaa1) by A3, A4, A5, FINSEQ_6:def 4;
hence ((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G by A3, A4, A5, A7, A8, A9, FINSEQ_6:def 4; :: thesis: verum

end;

hence (m,n) -cut W is Walk of G by Def3; :: thesis: verum

end;

thus ( ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W is Walk of G ) & ( for b₁ being Walk of G holds verum ) ) ; :: thesis: verum