:: deftheorem defines is_mincost_DPath_from GLIB_004:def 2 :
for G being real-weighted WGraph
for W being DPath of G
for x, y being set holds
( W is_mincost_DPath_from x,y iff ( W is_Walk_from x,y & ( for W2 being DPath of G st W2 is_Walk_from x,y holds
W .cost() <= W2 .cost() ) ) );