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 & EL has_valid_flow_from source,sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds
FF:PushFlow (EL,P) has_valid_flow_from source,sink