:: deftheorem Def18 defines FF:Step GLIB_005:def 18 :
for G being _finite natural-weighted WGraph
for EL being FF:ELabeling of G
for sink, source being Vertex of G holds
( ( sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = EL ) );