theorem Th14: :: GLIB_004:14

for G being _finite real-weighted WGraph
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() by Def3;