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;
then consider W2 being DPath of G such that
A2: ( W2 is_mincost_DPath_from x,y & G .min_DPath_cost x,y = W2 .cost() ) by Def3;
thus G .min_DPath_cost x,y = W .cost() by A1, A2, Th11; :: thesis: verum