let G be finite real-weighted WGraph; :: thesis: for EL being FF:ELabeling of
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)))
let EL be FF:ELabeling of ; :: thesis: 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)))
let source, sink be set ; :: thesis: 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)))
let V be Subset of (the_Vertices_of G); :: thesis: ( EL has_valid_flow_from source,sink & source in V & not sink in V implies EL .flow source,sink <= Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) )
assume A1: ( EL has_valid_flow_from source,sink & source in V & not sink in V ) ; :: thesis: EL .flow source,sink <= Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V)))
set E1 = EL | (G .edgesDBetween V,((the_Vertices_of G) \ V));
set E2 = EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V);
set W1 = (the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V));
set B1 = EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V);
A2: EL .flow source,sink = (Sum (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V))) by A1, Th11;

now

let e be set ; :: thesis: ( e in G .edgesDBetween V,((the_Vertices_of G) \ V) implies (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e <= ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e )
assume A3: e in G .edgesDBetween V,((the_Vertices_of G) \ V) ; :: thesis: (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e <= ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e
then ( (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e = EL . e & ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e = (the_Weight_of G) . e ) by FUNCT_1:72;
hence (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e <= ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e by A1, A3, Def7; :: thesis: verum

end;

then A4: Sum (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) <= Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) by GLIB_004:5;
A5: Sum (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) = 0 by UPROOTS:13;

now

let e be set ; :: thesis: ( e in G .edgesDBetween ((the_Vertices_of G) \ V),V implies (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . e <= (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . e )
assume A6: e in G .edgesDBetween ((the_Vertices_of G) \ V),V ; :: thesis: (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . e <= (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . e
EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V) = (G .edgesDBetween ((the_Vertices_of G) \ V),V) --> 0 by POLYNOM1:def 15;
hence (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . e <= (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . e by A6, FUNCOP_1:13; :: thesis: verum

end;

then 0 <= Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) by A5, GLIB_004:5;
then A8: (Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V))) <= (Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - 0 by XREAL_1:15;
(Sum (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V))) <= (Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V))) by A4, XREAL_1:11;
hence EL .flow source,sink <= Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) by A2, A8, XXREAL_0:2; :: thesis: verum