theorem Th12: :: GLIB_005:12

for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set
for V being Subset of (the_Vertices_of G) st EL has_valid_flow_from source,sink & source in V & not sink in V holds
EL .flow (source,sink) <= Sum ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V))))