let G be finite real-weighted WGraph; :: thesis: 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)))
let EL be FF:ELabeling of G; :: 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 that
A1: EL has_valid_flow_from source,sink and
A2: source in V and
A3: not sink in V ; :: thesis: EL .flow source,sink <= Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V)))
set W1 = (the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V));
set E2 = EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V);
set E1 = EL | (G .edgesDBetween V,((the_Vertices_of G) \ V));

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 A4: 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 A5: ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e = (the_Weight_of G) . e by FUNCT_1:72;
(EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . e = EL . e by A4, 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, A4, A5, Def2; :: thesis: verum

end;

then 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;
then A6: (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 XREAL_1:11;
set B1 = EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V);

A7: 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 )
A8: EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V) = (G .edgesDBetween ((the_Vertices_of G) \ V),V) --> 0 by PRE_POLY:def 13;
assume 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
hence (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . e <= (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . e by A8, FUNCOP_1:13; :: thesis: verum

end;

Sum (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) = 0 by UPROOTS:13;
then 0 <= Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) by A7, GLIB_004:5;
then A9: (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;
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, A2, A3, Th11;
hence EL .flow source,sink <= Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) by A9, A6, XXREAL_0:2; :: thesis: verum