for G being _finite natural-weighted WGraph
for source, sink being Vertex of G st sink <> source holds
FF:MaxFlow (G,source,sink) has_maximum_flow_from source,sink