let IT1, IT2 be Real; ( ( 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 ( ( 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
;
( 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
and A7:
IT1 = W1 .cost()
;
( 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 A8:
W2 is_mincost_DPath_from x,
y
and A9:
IT2 = W2 .cost()
;
IT1 = IT2
W2 is_Walk_from x,
y
by A8;
then A10:
IT1 <= IT2
by A6, A7, A9;
W1 is_Walk_from x,
y
by A6;
then
IT2 <= IT1
by A7, A8, A9;
hence
IT1 = IT2
by A10, XXREAL_0:1;
verum
end;
thus
( ( for W being DWalk of G holds not W is_Walk_from x,y ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 )
; verum