theorem Th24: :: GLIB_004:24

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