for G being real-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G
for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds
W .addEdge e is_augmenting_wrt EL