let G be real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for W being Walk of G
for m, n being Nat st W is_augmenting_wrt EL holds
W .cut (m,n) is_augmenting_wrt EL
let EL be FF:ELabeling of G; :: thesis: for W being Walk of G
for m, n being Nat st W is_augmenting_wrt EL holds
W .cut (m,n) is_augmenting_wrt EL
let W be Walk of G; :: thesis: for m, n being Nat st W is_augmenting_wrt EL holds
W .cut (m,n) is_augmenting_wrt EL
let m, n be Nat; :: thesis: ( W is_augmenting_wrt EL implies W .cut (m,n) is_augmenting_wrt EL )
set W2 = W .cut (m,n);
assume A1: W is_augmenting_wrt EL ; :: thesis: W .cut (m,n) is_augmenting_wrt EL

now :: thesis: W .cut (m,n) is_augmenting_wrt EL

per cases ( ( m is odd & n is odd & m <= n & n <= len W ) or not m is odd or not n is odd or not m <= n or not n <= len W ) ;

suppose A2: ( m is odd & n is odd & m <= n & n <= len W ) ; :: thesis: W .cut (m,n) is_augmenting_wrt EL

then reconsider m9 = m, n9 = n as odd Element of NAT by ORDINAL1:def 12;

now :: thesis: for x being odd Nat st x < len (W .cut (m,n)) holds
( ( (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1)) ) & ( not (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies 0 < EL . ((W .cut (m,n)) . (x + 1)) ) )

let x be odd Nat; :: thesis: ( x < len (W .cut (m,n)) implies ( ( (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1)) ) & ( not (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies 0 < EL . ((W .cut (m,n)) . (x + 1)) ) ) )
reconsider x9 = x as Element of NAT by ORDINAL1:def 12;
set v1b = (W .cut (m,n)) . x;
set eb = (W .cut (m,n)) . (x + 1);
set v2b = (W .cut (m,n)) . (x + 2);
assume A3: x < len (W .cut (m,n)) ; :: thesis: ( ( (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1)) ) & ( not (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies 0 < EL . ((W .cut (m,n)) . (x + 1)) ) )
then A4: x9 in dom (W .cut (m,n)) by GLIB_001:12;
A5: m9 <= n9 by A2;
A6: x9 + 2 in dom (W .cut (m,n)) by A3, GLIB_001:12;
then A7: (W .cut (m,n)) . (x9 + 2) = W . ((m9 + (x9 + 2)) - 1) by A2, A5, GLIB_001:47;
x9 + 1 in dom (W .cut (m,n)) by A3, GLIB_001:12;
then A8: (W .cut (m,n)) . (x9 + 1) = W . ((m9 + (x9 + 1)) - 1) by A2, A5, GLIB_001:47;
(m9 + x9) - 1 in dom W by A2, A4, A5, GLIB_001:47;
then reconsider a = (m9 + x) - 1, a2 = (m + (x + 2)) - 1 as Element of NAT by A8;
reconsider a = a as odd Element of NAT ;
set v1a = W . a;
set ea = W . (a + 1);
set v2a = W . (a + 2);
(m9 + (x9 + 2)) - 1 in dom W by A2, A6, A5, GLIB_001:47;
then a2 <= len W by FINSEQ_3:25;
then A9: ((m + (x + 2)) - 1) - 2 < (len W) - 0 by XREAL_1:15;

hereby :: thesis: ( not (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies 0 < EL . ((W .cut (m,n)) . (x + 1)) )

assume (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G ; :: thesis: EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1))
then W . (a + 1) DJoins W . a,W . (a + 2),G by A2, A4, A5, A8, A7, GLIB_001:47;
hence EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1)) by A1, A8, A9; :: thesis: verum

end;

assume not (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G ; :: thesis: 0 < EL . ((W .cut (m,n)) . (x + 1))
then not W . (a + 1) DJoins W . a,W . (a + 2),G by A2, A4, A5, A8, A7, GLIB_001:47;
hence 0 < EL . ((W .cut (m,n)) . (x + 1)) by A1, A8, A9; :: thesis: verum

end;

hence W .cut (m,n) is_augmenting_wrt EL ; :: thesis: verum

end;

suppose ( not m is odd or not n is odd or not m <= n or not n <= len W ) ; :: thesis: W .cut (m,n) is_augmenting_wrt EL

hence W .cut (m,n) is_augmenting_wrt EL by A1, GLIB_001:def 11; :: thesis: verum

end;

end;

end;

hence W .cut (m,n) is_augmenting_wrt EL ; :: thesis: verum