let G be finite real-weighted WGraph; :: thesis: for W being DPath of G
for x, y being set st W is_mincost_DPath_from x,y holds
G .min_DPath_cost (x,y) = W .cost()
let W be DPath of G; :: thesis: for x, y being set st W is_mincost_DPath_from x,y holds
G .min_DPath_cost (x,y) = W .cost()
let x, y be set ; :: thesis: ( W is_mincost_DPath_from x,y implies G .min_DPath_cost (x,y) = W .cost() )
assume A1: W is_mincost_DPath_from x,y ; :: thesis: G .min_DPath_cost (x,y) = W .cost()
then W is_Walk_from x,y by Def2;
hence G .min_DPath_cost (x,y) = W .cost() by A1, Def3; :: thesis: verum