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 and
A7: 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 A8: W2 is_mincost_DPath_from x,y and
A9: IT2 = W2 .cost() ; :: thesis: 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; :: 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