theorem Th24: :: GLIB_004:24

for G being _finite real-weighted WGraph
for s being Vertex of G holds DIJK:CompSeq s is halting