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_{1} being Walk of G holds verum ) )

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

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

hence
(m,n) -cut W is Walk of G
by Def3; :: thesis: verum((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;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