theorem Th15: :: GLIB_005:15

for G being _finite natural-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set
for P being Path of G st source <> sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds
(EL .flow (source,sink)) + (P .tolerance EL) = (FF:PushFlow (EL,P)) .flow (source,sink)