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 b1 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 ;
then ((len ((m,n) -cut W)) + m4) - m4 = (n4 + 1) - m4 by ;
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 ;
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 ;
m <= len W by ;
then W . m = W .vertexAt m by ;
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 ;
reconsider iaa1 = i - 1 as even Element of NAT by ;
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 ;
i + m < (len ((m,n) -cut W)) + m by ;
then i + m < n + 1 by ;
then i + m4 <= n4 by NAT_1:13;
then m4 + i < n4 by XXREAL_0:1;
then m + i < len W by ;
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 ;
then ((m,n) -cut W) . (iaa1 + 1) = W . (m + iaa1) by ;
hence ((m,n) -cut W) . (i + 1) Joins ((m,n) -cut W) . i,((m,n) -cut W) . (i + 2),G by ; :: 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 b1 being Walk of G holds verum ) ) ; :: thesis: verum