for G being _finite natural-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set st EL has_valid_flow_from source,sink & ( for P being Path of G holds
( not P is_Walk_from source,sink or not P is_augmenting_wrt EL ) ) holds
EL has_maximum_flow_from source,sink