theorem Th13: :: GLIB_005:13

for G being _finite natural-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G st W is trivial & W is_augmenting_wrt EL holds
0 < W .tolerance EL