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 :: thesis: for e being set st e in G .edgesDBetween (V,((the_Vertices_of G) \ V)) holds
(EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . e <= ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . e
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:49;
(EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . e = EL . e by A4, FUNCT_1:49;
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; :: 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:9;
set B1 = EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V));
A7: now :: thesis: for e being set st e in G .edgesDBetween (((the_Vertices_of G) \ V),V) holds
(EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . e <= (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . e
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 PBOOLE:def 3;
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:7; :: thesis: verum
end;
Sum (EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V))) = 0 by UPROOTS:11;
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:13;
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