:: deftheorem defines is_mincost_DTree_rooted_at GLIB_004:def 1 :
for G1 being real-weighted WGraph
for G2 being WSubgraph of G1
for v being set holds
( G2 is_mincost_DTree_rooted_at v iff ( G2 is Tree-like & ( for x being Vertex of G2 ex W2 being DPath of G2 st
( W2 is_Walk_from v,x & ( for W1 being DPath of G1 st W1 is_Walk_from v,x holds
W2 .cost() <= W1 .cost() ) ) ) ) );