let G be finite real-weighted WGraph; :: thesis: for W1, W2 being DPath of G
for x, y being set st W1 is_mincost_DPath_from x,y & W2 is_mincost_DPath_from x,y holds
W1 .cost() = W2 .cost()
let W1, W2 be DPath of G; :: thesis: for x, y being set st W1 is_mincost_DPath_from x,y & W2 is_mincost_DPath_from x,y holds
W1 .cost() = W2 .cost()
let x, y be set ; :: thesis: ( W1 is_mincost_DPath_from x,y & W2 is_mincost_DPath_from x,y implies W1 .cost() = W2 .cost() )
assume A1: ( W1 is_mincost_DPath_from x,y & W2 is_mincost_DPath_from x,y ) ; :: thesis: W1 .cost() = W2 .cost()
then A2: ( 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 Def2;
( 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 A1, Def2;
then ( W1 .cost() <= W2 .cost() & W2 .cost() <= W1 .cost() ) by A2;
hence W1 .cost() = W2 .cost() by XXREAL_0:1; :: thesis: verum