theorem Th1: :: GLIB_005:1

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