let G be _finite natural-weighted WGraph; :: thesis:
let EL be FF:ELabeling of G; :: thesis:
let source, sink be set ; :: thesis:
assume that
A1: EL has_valid_flow_from source,sink and
A2: for P being Path of G holds
( not P is_Walk_from source,sink or not P is_augmenting_wrt EL ) ; :: thesis:
reconsider src = source as Vertex of G by A1;
set CS = AP:CompSeq (EL,src);
set Gn = AP:FindAugPath (EL,src);
set Gn1 = (AP:CompSeq (EL,src)) . (((AP:CompSeq (EL,src)) .Lifespan()) + 1);
reconsider V = dom (AP:FindAugPath (EL,src)) as Subset of (the_Vertices_of G) ;
set E1 = G .edgesDBetween (V,((the_Vertices_of G) \ V));
set A1 = EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)));
set B1 = (the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)));
set e = the Element of AP:NextBestEdges (AP:FindAugPath (EL,src));
AP:CompSeq (EL,src) is halting by Th6;
then A3: (AP:CompSeq (EL,src)) . (((AP:CompSeq (EL,src)) .Lifespan()) + 1) = AP:FindAugPath (EL,src) by GLIB_000:def 56;
A4: (AP:CompSeq (EL,src)) . (((AP:CompSeq (EL,src)) .Lifespan()) + 1) = AP:Step (AP:FindAugPath (EL,src)) by Def12;

A5: now :: thesis:

assume A6: AP:NextBestEdges (AP:FindAugPath (EL,src)) <> {} ; :: thesis:

now :: thesis:

per cases by A6, Def9;

suppose A7: the Element of AP:NextBestEdges (AP:FindAugPath (EL,src)) is_forward_edge_wrt AP:FindAugPath (EL,src) ; :: thesis:

then (the_Source_of G) . the Element of AP:NextBestEdges (AP:FindAugPath (EL,src)) in V ;
then A8: AP:FindAugPath (EL,src) = (AP:FindAugPath (EL,src)) +* (((the_Target_of G) . the Element of AP:NextBestEdges (AP:FindAugPath (EL,src))) .--> the Element of AP:NextBestEdges (AP:FindAugPath (EL,src))) by A4, A3, A6, Def10;
not (the_Target_of G) . the Element of AP:NextBestEdges (AP:FindAugPath (EL,src)) in V by A7;
hence contradiction by A8, Lm2; :: thesis:

end;

suppose the Element of AP:NextBestEdges (AP:FindAugPath (EL,src)) is_backward_edge_wrt AP:FindAugPath (EL,src) ; :: thesis:

then A9: not (the_Source_of G) . the Element of AP:NextBestEdges (AP:FindAugPath (EL,src)) in V ;
then AP:FindAugPath (EL,src) = (AP:FindAugPath (EL,src)) +* (((the_Source_of G) . the Element of AP:NextBestEdges (AP:FindAugPath (EL,src))) .--> the Element of AP:NextBestEdges (AP:FindAugPath (EL,src))) by A4, A3, A6, Def10;
hence contradiction by A9, Lm2; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

A10: now :: thesis:

let x be set ; :: thesis:
assume A11: x in G .edgesDBetween (V,((the_Vertices_of G) \ V)) ; :: thesis:
then A12: (EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x = EL . x by FUNCT_1:49;
A13: x DSJoins V,(the_Vertices_of G) \ V,G by A11, GLIB_000:def 31;
then (the_Target_of G) . x in (the_Vertices_of G) \ V ;
then A14: not (the_Target_of G) . x in V by XBOOLE_0:def 5;
A15: ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x = (the_Weight_of G) . x by A11, FUNCT_1:49;
A16: (the_Source_of G) . x in V by A13;

A17: now :: thesis:

assume (EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x < ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x ; :: thesis:
then x is_forward_edge_wrt AP:FindAugPath (EL,src) by A11, A12, A15, A16, A14;
hence contradiction by A5, Def9; :: thesis:

end;

(EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x <= ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x by A1, A11, A12, A15;
hence (EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x = ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x by A17, XXREAL_0:1; :: thesis:

end;

set E2 = G .edgesDBetween (((the_Vertices_of G) \ V),V);
set A2 = EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V));
set B2 = EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V));

now :: thesis:

let x be set ; :: thesis:
assume A18: x in G .edgesDBetween (((the_Vertices_of G) \ V),V) ; :: thesis:
then A19: x DSJoins (the_Vertices_of G) \ V,V,G by GLIB_000:def 31;
then A20: (the_Target_of G) . x in V ;
(the_Source_of G) . x in (the_Vertices_of G) \ V by A19;
then A21: not (the_Source_of G) . x in V by XBOOLE_0:def 5;
A22: (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x = EL . x by A18, FUNCT_1:49;

A23: now :: thesis:

assume 0 < (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x ; :: thesis:
then x is_backward_edge_wrt AP:FindAugPath (EL,src) by A18, A22, A20, A21;
hence contradiction by A5, Def9; :: thesis:

end;

EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V)) = (G .edgesDBetween (((the_Vertices_of G) \ V),V)) --> 0 by PBOOLE:def 3;
then (EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x = 0 by A18, FUNCOP_1:7;
hence (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x = (EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x by A23; :: thesis:

end;

then Sum (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) = Sum (EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V))) by GLIB_004:6;
then A24: Sum (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) = 0 by UPROOTS:11;
A25: not sink in dom (AP:FindAugPath (EL,src)) by A2, Th9;
then 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, Th10, Th11;
then EL .flow (source,sink) = Sum ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) by A10, A24, GLIB_004:6;
then for X being FF:ELabeling of G st X has_valid_flow_from source,sink holds
X .flow (source,sink) <= EL .flow (source,sink) by A25, Th10, Th12;
hence EL has_maximum_flow_from source,sink by A1; :: thesis: