:: deftheorem defines DIJK:SSSP GLIB_004:def 12 :
for G being real-weighted WGraph
for src being Vertex of G holds DIJK:SSSP (G,src) = (DIJK:CompSeq src) .Result() ;