let G be real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for W being Walk of G st W is trivial holds
W is_augmenting_wrt EL
let EL be FF:ELabeling of G; :: thesis: for W being Walk of G st W is trivial holds
W is_augmenting_wrt EL
let W be Walk of G; :: thesis: ( W is trivial implies W is_augmenting_wrt EL )
assume A1: W is trivial ; :: thesis: W is_augmenting_wrt EL

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

let n be odd Nat; :: thesis: ( n < len W implies ( ( W . (n + 1) DJoins W . n,W . (n + 2),G implies EL . (W . (n + 1)) < (the_Weight_of G) . (W . (n + 1)) ) & ( not W . (n + 1) DJoins W . n,W . (n + 2),G implies 0 < EL . (W . (n + 1)) ) ) )
assume n < len W ; :: thesis: ( ( W . (n + 1) DJoins W . n,W . (n + 2),G implies EL . (W . (n + 1)) < (the_Weight_of G) . (W . (n + 1)) ) & ( not W . (n + 1) DJoins W . n,W . (n + 2),G implies 0 < EL . (W . (n + 1)) ) )
then n < 1 by A1, GLIB_001:126;
hence ( ( W . (n + 1) DJoins W . n,W . (n + 2),G implies EL . (W . (n + 1)) < (the_Weight_of G) . (W . (n + 1)) ) & ( not W . (n + 1) DJoins W . n,W . (n + 2),G implies 0 < EL . (W . (n + 1)) ) ) by ABIAN:12; :: thesis: verum

end;

hence W is_augmenting_wrt EL ; :: thesis: verum