theorem Th8: :: GLIB_005:8

for G being real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G
for n being Nat
for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) )