let G be finite natural-weighted WGraph; :: thesis: for source, sink being Vertex of G st sink <> source holds
FF:MaxFlow G,source,sink has_maximum_flow_from source,sink
let source, sink be Vertex of G; :: thesis: ( sink <> source implies FF:MaxFlow G,source,sink has_maximum_flow_from source,sink )
set CS = FF:CompSeq G,source,sink;
set n = (FF:CompSeq G,source,sink) .Lifespan() ;
set Gn = (FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() );
set Gn1 = (FF:CompSeq G,source,sink) . (((FF:CompSeq G,source,sink) .Lifespan() ) + 1);
A1: (FF:CompSeq G,source,sink) . (((FF:CompSeq G,source,sink) .Lifespan() ) + 1) = FF:Step ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),source,sink by Def20;
assume A2: sink <> source ; :: thesis: FF:MaxFlow G,source,sink has_maximum_flow_from source,sink
then FF:CompSeq G,source,sink is halting by Th17;
then A3: (FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() ) = (FF:CompSeq G,source,sink) . (((FF:CompSeq G,source,sink) .Lifespan() ) + 1) by GLIB_000:def 57;

now

given P being Path of G such that A4: P is_Walk_from source,sink and
A5: P is_augmenting_wrt (FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() ) ; :: thesis: contradiction
set P = AP:GetAugPath ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),source,sink;
A6: sink in dom (AP:FindAugPath ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),source) by A4, A5, Th9;
then A7: AP:GetAugPath ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),source,sink is_Walk_from source,sink by Def14;
then A8: (AP:GetAugPath ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),source,sink) .first() = source by GLIB_001:def 23;
A9: (AP:GetAugPath ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),source,sink) .last() = sink by A7, GLIB_001:def 23;
A10: AP:GetAugPath ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),source,sink is_augmenting_wrt (FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() ) by A6, Def14;
(FF:CompSeq G,source,sink) . (((FF:CompSeq G,source,sink) .Lifespan() ) + 1) = FF:PushFlow ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),(AP:GetAugPath ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),source,sink) by A1, A6, Def18;
then (((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )) .flow source,sink) + ((AP:GetAugPath ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() )),source,sink) .tolerance ((FF:CompSeq G,source,sink) . ((FF:CompSeq G,source,sink) .Lifespan() ))) = ((FF:CompSeq G,source,sink) . (((FF:CompSeq G,source,sink) .Lifespan() ) + 1)) .flow source,sink by A2, A7, A10, Th15;
hence contradiction by A2, A3, A8, A9, A10, Th13, GLIB_001:128; :: thesis: verum

end;

hence FF:MaxFlow G,source,sink has_maximum_flow_from source,sink by A2, Th16, Th18; :: thesis: verum