for G being _finite nonnegative-weighted WGraph
for s being Vertex of G
for G2 being inducedWSubgraph of G, dom ((DIJK:SSSP (G,s)) `1),(DIJK:SSSP (G,s)) `2 holds
( G2 is_mincost_DTree_rooted_at s & ( for v being Vertex of G st v in G .reachableDFrom s holds
( v in the_Vertices_of G2 & G .min_DPath_cost (s,v) = ((DIJK:SSSP (G,s)) `1) . v ) ) )