for G being real-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G st W is V5() holds
W is_augmenting_wrt EL