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 that
A1: W1 is_mincost_DPath_from x,y and
A2: W2 is_mincost_DPath_from x,y ; :: thesis: W1 .cost() = W2 .cost()
W2 is_Walk_from x,y by A2;
then A3: W1 .cost() <= W2 .cost() by A1;
W1 is_Walk_from x,y by A1;
then W2 .cost() <= W1 .cost() by A2;
hence W1 .cost() = W2 .cost() by A3, XXREAL_0:1; :: thesis: verum