:: deftheorem defines DIJK:Init GLIB_004:def 9 :
for G being real-weighted WGraph
for src being Vertex of G holds DIJK:Init src = [(src .--> 0),{}];