let G be finite natural-weighted WGraph; :: thesis: for EL being FF:ELabeling of
for W being Walk of G st not W is trivial & W is_augmenting_wrt EL holds
0 < W .tolerance EL
let EL be FF:ELabeling of ; :: thesis: for W being Walk of G st not W is trivial & W is_augmenting_wrt EL holds
0 < W .tolerance EL
let W be Walk of G; :: thesis: ( not W is trivial & W is_augmenting_wrt EL implies 0 < W .tolerance EL )
assume that
A1: not W is trivial and
A1a: W is_augmenting_wrt EL ; :: thesis: 0 < W .tolerance EL
set T = W .tolerance EL;
( W .tolerance EL in rng (W .flowSeq EL) & ( for k being real number st k in rng (W .flowSeq EL) holds
W .tolerance EL <= k ) ) by A1, A1a, Def19;
then consider n being Nat such that
A2: ( n in dom (W .flowSeq EL) & W .tolerance EL = (W .flowSeq EL) . n ) by FINSEQ_2:11;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
dom (W .flowSeq EL) = dom (W .edgeSeq() ) by A1a, Def18;
then 2 * n in dom W by A2, GLIB_001:79;
then A3: ( 1 <= 2 * n & 2 * n <= len W ) by FINSEQ_3:27;
then reconsider 2n1 = (2 * n) - 1 as odd Element of NAT by INT_1:18;
A4: (2 * n) - 1 < (len W) - 0 by A3, XREAL_1:17;
set v1 = W . 2n1;
set e = W . (2 * n);
set v2 = W . ((2 * n) + 1);
A5: ( ((2 * n) - 1) + 1 = 2 * n & ((2 * n) - 1) + 2 = (2 * n) + 1 ) ;

now

per cases ( W . (2 * n) DJoins W . 2n1,W . ((2 * n) + 1),G or not W . (2 * n) DJoins W . 2n1,W . ((2 * n) + 1),G ) ;

suppose A6: W . (2 * n) DJoins W . 2n1,W . ((2 * n) + 1),G ; :: thesis: 0 < W .tolerance EL

then A7: W .tolerance EL = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) by A1a, A2, Def18;
EL . (W . (2 * n)) < (the_Weight_of G) . (W . (2 * n)) by A1a, A4, A5, A6, Def12;
then (EL . (W . (2 * n))) - (EL . (W . (2 * n))) < W .tolerance EL by A7, XREAL_1:16;
hence 0 < W .tolerance EL ; :: thesis: verum

end;

suppose A8: not W . (2 * n) DJoins W . 2n1,W . ((2 * n) + 1),G ; :: thesis: 0 < W .tolerance EL

then W .tolerance EL = EL . (W . (2 * n)) by A1a, A2, Def18;
hence 0 < W .tolerance EL by A1a, A4, A5, A8, Def12; :: thesis: verum

end;

end;

end;

hence 0 < W .tolerance EL ; :: thesis: verum