let IT1, IT2 be Real; :: thesis: ( ( ex W being DWalk of G st W is_Walk_from x,y & ex W being DPath of G st
( W is_mincost_DPath_from x,y & IT1 = W .cost() ) & ex W being DPath of G st
( W is_mincost_DPath_from x,y & IT2 = W .cost() ) implies IT1 = IT2 ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )
hereby :: thesis: ( ( for W being DWalk of G holds not W is_Walk_from x,y ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 )
assume
ex
W being
DWalk of
G st
W is_Walk_from x,
y
;
:: thesis: ( ex W1 being DPath of G st
( W1 is_mincost_DPath_from x,y & IT1 = W1 .cost() ) & ex W2 being DPath of G st
( W2 is_mincost_DPath_from x,y & IT2 = W2 .cost() ) implies IT1 = IT2 )given W1 being
DPath of
G such that A6:
(
W1 is_mincost_DPath_from x,
y &
IT1 = W1 .cost() )
;
:: thesis: ( ex W2 being DPath of G st
( W2 is_mincost_DPath_from x,y & IT2 = W2 .cost() ) implies IT1 = IT2 )given W2 being
DPath of
G such that A7:
(
W2 is_mincost_DPath_from x,
y &
IT2 = W2 .cost() )
;
:: thesis: IT1 = IT2A8:
(
W1 is_Walk_from x,
y & ( for
W2 being
DPath of
G st
W2 is_Walk_from x,
y holds
W1 .cost() <= W2 .cost() ) )
by A6, Def2;
A9:
(
W2 is_Walk_from x,
y & ( for
W1 being
DPath of
G st
W1 is_Walk_from x,
y holds
W2 .cost() <= W1 .cost() ) )
by A7, Def2;
A10:
IT2 <= IT1
by A6, A7, A8, Def2;
IT1 <= IT2
by A6, A7, A9, Def2;
hence
IT1 = IT2
by A10, XXREAL_0:1;
:: thesis: verum
end;
thus
( ( for W being DWalk of G holds not W is_Walk_from x,y ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 )
; :: thesis: verum