:: deftheorem defines has_maximum_flow_from GLIB_005:def 4 :
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set holds
( EL has_maximum_flow_from source,sink iff ( EL has_valid_flow_from source,sink & ( for E2 being FF:ELabeling of G st E2 has_valid_flow_from source,sink holds
E2 .flow (source,sink) <= EL .flow (source,sink) ) ) );